Require Import logical.
Require Import algebra.
Require Import naturals.
Require Import fractions.
Require Import prats.
Require Import cuts.

(** Structure of the Real Numbers *)

(** Definition of the Real Numbers *)

Inductive real : Type :=
| Z : real
| P : cut -> real
| N : cut -> real.

(** Order of the Real Numbers *)

Definition abs_real (x:real) := match x with
| N a => P a
| x => x
end.

Definition lt_real (x y :real) := match x,y with
| P a, P b => a < b
| P _, _ => False
| Z, P _ => True
| Z, _ => False
| N a, N b => b < a
| N _, _ => True
end.
Notation "x < y":=(lt_real x y).

Theorem satz167H0 : trichotomy real lt_real.
intros [|x|x] [|y|y]; try(simpl;tauto).
destruct (@satz123H0 x y) as [H|[H|H]]; try tauto.
right. left. apply (f_equal P H).
destruct (@satz123H0 x y) as [H|[H|H]]; try tauto.
right. left. apply (f_equal N H).
Qed.

Lemma satz167H1 (x y:real) : y < x -> x = y -> False.
intros [|x|x] [|y|y] A B; try (simpl;tauto); try discriminate B.
injection B; intros C.
apply (satz123H3 A C).
injection B; intros C.
apply (satz123H1 A C).
Qed.

Lemma satz167H2 (x y:real) : x < y -> y < x -> False.
intros [|x|x] [|y|y] A B; try (simpl;tauto).
apply (satz123H2 A B).
apply (satz123H2 A B).
Qed.

Lemma satz167H3 (x y:real) : x < y -> x = y -> False.
intros x y A B.
symmetry in B.
apply (satz167H1 _ _ A B).
Qed.

Definition leq_real (x y:real) := x < y \/ x = y.
Notation "x <= y":=(leq_real x y).

Theorem satz170 {x:real} : Z <= abs_real x.
unfold abs_real.
intros [|x|x]. right. reflexivity.
left. exact I. left. exact I.
Qed.

Theorem satz171 : transitive real lt_real.
intros [|x|x] [|y|y] [|z|z]; try tauto.
intros []. apply satz126.
intros [].
intros _ [].
intros _ [].
intros A B. apply (satz126 _ _ _ B A).
Qed.

Theorem satz172a {x y z:real} : x <= y -> y < z -> x < z.
intros x y z [A|A] B.
apply (satz171 _ _ _ A B).
rewrite A. apply B.
Qed.

Theorem satz172b {x y z:real} : x < y -> y <= z -> x < z.
intros x y z A [B|B].
apply (satz171 _ _ _ A B).
rewrite <-B. apply A.
Qed.


Theorem satz173 : transitive real (fun x y => x <= y).
intros x y z A [B|B].
left. apply (satz172a A B).
rewrite <-B. apply A.
Qed.

Definition is_rational_real (x:real) := match x with
| P a => is_rational_cut a
| Z => True
| N a => is_rational_cut a
end.

Definition is_irrational_real (x:real) := ~ is_rational_real x.

Variable str : STR cut lt_cut.

(** In this section we discuss the necessity of STR as additional assumption.
One can read in another file that STR <-> SXM and SXM -> XM *)

Section STRNec.

(** Assuming we have addition with the following three properties, we have STR cut lt_cut *)

Variable add_real : real -> real -> real.
Variable add_real_PN1 : forall (a b:cut) (l:a = b), add_real (P a) (N b) = Z.
Variable add_real_PN2 : forall (a b:cut) (l:lt_cut a b), add_real (P a) (N b) = N (sub_cut b a l).
Variable add_real_PN3 : forall (a b:cut) (l:lt_cut b a), add_real (P a) (N b) = P (sub_cut a b l).

Definition strongTrich : STR cut lt_cut.
intros a b.
case_eq (add_real (P a) (N b)).
intros e. right.
destruct (satz123H0 a b) as [H|[H|H]].
 rewrite (add_real_PN2 a b H) in e. discriminate e.
 exact H.
 rewrite (add_real_PN3 a b H) in e. discriminate e.
intros c e. left. right.
destruct (satz123H0 a b) as [H|[H|H]].
 rewrite (add_real_PN2 a b H) in e. discriminate e.
 rewrite (add_real_PN1 a b H) in e. discriminate e.
 exact H.
intros c e. left. left.
destruct (satz123H0 a b) as [H|[H|H]].
 exact H.
 rewrite (add_real_PN1 a b H) in e. discriminate e.
 rewrite (add_real_PN3 a b H) in e. discriminate e.
Qed.

End STRNec.

Lemma str_equiv_a (a b:cut) (l:lt_cut a b) :  str a b = inleft (a=b) (left (lt_cut b a) l).
intros a b A. destruct (str a b) as [[B|B]|B].
rewrite (CE_PI ce _ A B). tauto.
destruct (satz123H2 A B).
destruct (satz123H1 A B).
Qed.

Lemma str_equiv_b (a b:cut) (l:lt_cut b a) : str a b = inleft (a=b) (right (lt_cut a b) l).
intros a b A. destruct (str a b) as [[B|B]|B].
destruct (satz123H2 A B).
rewrite (CE_PI ce _ A B). tauto.
destruct (satz123H3 A B).
Qed.

Lemma str_equiv_c (a b:cut) (l:a=b): str a b = inright (sumbool (lt_cut a b) (lt_cut b a)) l.
intros a b A. destruct (str a b) as [[B|B]|B].
destruct (satz123H1 B A).
destruct (satz123H3 B A).
rewrite (CE_PI ce _ A B). tauto.
Qed.


(** Addition of Real Numbers *)

Definition add_real (x y:real):real := match x,y with
| Z, y => y
| x, Z => x
| P a, P b => P (a + b)
| P a, N b => match str a b with | inright _ => Z
                                 | inleft (left l) => N (sub_cut b a l)
                                 | inleft (right l) => P (sub_cut a b l) end
| N a, P b => match str a b with | inright _ => Z
                                 | inleft (left l) => P (sub_cut b a l)
                                 | inleft (right l) => N (sub_cut a b l) end
| N a, N b => N (a + b)
end.
Notation "x + y":=(add_real x y).

Theorem satz175 : commutative real add_real.
unfold commutative.
intros [|x|x] [|y|y]; try tauto; simpl.
apply (f_equal P (satz130 _ _)).
destruct (str x y) as [[A|A]|A].
rewrite (str_equiv_b _ _ A). tauto.
rewrite (str_equiv_a _ _ A). tauto.
symmetry in A.
rewrite (str_equiv_c _ _ A). tauto.
destruct (str x y) as [[A|A]|A].
rewrite (str_equiv_b _ _ A). tauto.
rewrite (str_equiv_a _ _ A). tauto.
symmetry in A.
rewrite (str_equiv_c _ _ A). tauto.
apply (f_equal N (satz130 _ _)).
Qed.

Definition inv_add_real (x:real) := match x with
| Z => Z
| P a => N a
| N a => P a
end.

Definition sub_real (x y:real) := add_real x (inv_add_real y).
Notation "x - y":=(sub_real x y).

Theorem satz177 {x:real} : inv_add_real (inv_add_real x) = x.
intros []; unfold inv_add_real; tauto.
Qed.

Theorem satz178 {x:real} : abs_real (inv_add_real x) = abs_real x.
intros []; unfold inv_add_real,abs_real; tauto.
Qed.

Theorem satz179 {x:real} : (inv_add_real x) + x = Z.
intros [|x|x]; simpl. tauto.
rewrite (str_equiv_c _ _ (refl_equal x)).
tauto.
rewrite (str_equiv_c _ _ (refl_equal x)).
tauto.
Qed.

Theorem satz180 {x y:real} : inv_add_real (x + y) = inv_add_real x + inv_add_real y.
intros [][]; try tauto; intros d; unfold inv_add_real,add_real.
destruct (str c d) as [[A|A]|A]; reflexivity.
destruct (str c d) as [[B|B]|B]; reflexivity.
Qed.

Theorem satz181 {x y:real} : inv_add_real (x - y) = y - x.
intros x y. unfold sub_real. rewrite satz180,satz177.
apply satz175.
Qed.

Theorem satz182a {x y:real} : Z < x - y -> y < x.
intros [|a|a] [|b|b]; try tauto; simpl;
destruct (str a b) as [[A|A]|A]; tauto.
Qed.

Theorem satz182b {x y:real} : Z = x - y -> x = y.
intros [|a|a] [|b|b]; simpl; try tauto;
intros A;
try destruct (str a b) as [[B|B]|B]; try discriminate A.
apply (f_equal P B).
apply (f_equal N B).
Qed.

Theorem satz182c {x y:real} : x - y < Z -> x < y.
intros [|a|a] [|b|b]; try tauto; simpl;
destruct (str a b) as [[A|A]|A];
try tauto; intros [].
Qed.

Theorem satz182d {x y:real} : y < x -> Z < x - y.
intros x y; destruct (satz167H0 Z (x-y)) as [A|[A|A]]; intros B.
apply A.
destruct (satz167H1 _ _ B (satz182b A)).
destruct (satz167H2 _ _ B (satz182c A)).
Qed.

Theorem satz182e {x y:real} : x = y -> Z = x - y.
intros x y A. rewrite A.
unfold sub_real.
rewrite satz175,satz179. tauto.
Qed.

Theorem satz182f {x y:real} : x < y -> x - y < Z.
intros x y; destruct (satz167H0 Z (x-y)) as [A|[A|A]]; intros B.
destruct (satz167H2 _ _ B (satz182a A)).
destruct (satz167H3 _ _ B (satz182b A)).
apply A.
Qed.

Theorem satz183a {x y:real} : x < y -> inv_add_real y < inv_add_real x.
intros [|a|a] [|b|b]; try tauto; intros [].
Qed.

Theorem satz183b {x y:real} : x = y -> inv_add_real x = inv_add_real y.
intros x y A. rewrite A. tauto.
Qed.

Coercion cut_to_real (x:cut) := P x.

Theorem satz184 (x:real) : exists a, exists b, x = P a - P b.
intros [|a|a]. exists O. exists O. simpl.
rewrite (str_equiv_c O O (@refl_equal cut O)). tauto.
exists (add_cut O a). exists O. simpl.
rewrite (str_equiv_b _ _ (satz133)).
apply (f_equal P).
apply (@satz136b _ _ O). rewrite (satz130 (sub_cut _ _ _)),
sub_cut_correct_a. apply satz130.
exists O. exists (add_cut O a). simpl.
rewrite (str_equiv_a _ _ (satz133)).
apply (f_equal N).
apply (@satz136b _ _ O). rewrite (satz130 (sub_cut _ _ _)),
sub_cut_correct_a. apply satz130.
Qed.

Theorem satz185H0 {a a1 a2:cut} : @eq real a (a1 - a2) -> a2 < a1.
intros a a1 a2 A. simpl in A.
destruct (str a1 a2) as [[B|B]|B]; try discriminate A.
apply B.
Qed.

Theorem satz185H1 {a b a1 a2 b1 b2:cut} : 
   P a = a1 - a2 -> P b = b1 - b2 -> P a + P b = (a1 + b1) - (a2 + b2).
intros a b a1 a2 b1 b2 A B. simpl.
generalize (satz137 (satz185H0 A) (satz185H0 B)); intros C.
rewrite (str_equiv_b _ _ C).
apply (f_equal P).
apply (@satz136b _ _ (add_cut a2 b2)).
rewrite (satz130 (sub_cut _ _ _) _).
rewrite sub_cut_correct_a.
simpl in *.
destruct (str a1 a2) as [[D|D]|D]; try discriminate A.
destruct (str b1 b2) as [[E|E]|E]; try discriminate B.
injection A; clear A; intros A.
injection B; clear B; intros B.
rewrite A,B.
rewrite (satz130 _ (add_cut a2 b2)),satz131,(satz130 (sub_cut _ _ _)),<-(satz131 b2).
rewrite sub_cut_correct_a.
rewrite <-satz131,(satz130 a2),satz131.
rewrite sub_cut_correct_a.
apply satz130.
Qed.

Theorem satz185H2 {a b a1 a2 b1 b2:cut} : 
   P a = a1 - a2 -> N b = b1 - b2 -> P a + N b = (a1 + b1) - (a2 + b2).
intros a b a1 a2 b1 b2 A B. simpl in *.
destruct (str a1 a2) as [[C|C]|C]; try discriminate A.
destruct (str b1 b2) as [[D|D]|D]; try discriminate B.
injection A; clear A; intros A.
injection B; clear B; intros B.
generalize (satz137 C D); intros E.
destruct (str a b) as [[F|F]|F].
subst a. subst b. 
generalize (@satz134 _ _ a2 F); intros A. 
rewrite (satz130 (sub_cut a1 _ _)),sub_cut_correct_a in A.
generalize (@satz134 _ _ b1 A); intros B.
rewrite (satz130 (add_cut (sub_cut _ _ _) _)),<-satz131 in B.
rewrite sub_cut_correct_a,(satz130 _ a2) in B.
rewrite (str_equiv_a _ _ B).
apply (f_equal N).
apply (@satz136b _ _ (add_cut a1 b1)).
repeat rewrite (satz130 _ (add_cut a1 b1)).
rewrite sub_cut_correct_a.
apply (@satz136b _ _ (sub_cut a1 a2 C)).
rewrite satz131,(satz130 (sub_cut _ _ _)),sub_cut_correct_a.
apply (@satz136b _ _ a2).
rewrite (satz131 (add_cut a2 b2)),(satz130 (sub_cut a1 _ _)),
sub_cut_correct_a,(satz130 _ a2),<-satz131.
apply (@satz136b _ _ b1).
rewrite (satz131 (add_cut a2 _)),(satz130 (sub_cut _ _ _)),
sub_cut_correct_a.
rewrite satz131,(satz130 (add_cut a1 b1)),<-satz131,<-satz131.
reflexivity.
subst a. subst b. 
generalize (@satz134 _ _ a2 F); intros A. 
rewrite (satz130 (sub_cut a1 _ _)),sub_cut_correct_a in A.
generalize (@satz134 _ _ b1 A); intros B.
rewrite (satz130 (add_cut (sub_cut _ _ _) _)),<-satz131 in B.
rewrite sub_cut_correct_a,(satz130 _ a2) in B.
rewrite (str_equiv_b _ _ B).
apply (f_equal P).
apply (@satz136b _ _ (add_cut a2 b2)).
repeat rewrite (satz130 _ (add_cut a2 b2)).
rewrite sub_cut_correct_a.
apply (@satz136b _ _ (sub_cut b2 b1 D)).
rewrite satz131,(satz130 (sub_cut _ _ _)),sub_cut_correct_a.
apply (@satz136b _ _ b1).
rewrite (satz131 (add_cut a1 b1)), (satz130 (sub_cut b2 _ _)),
sub_cut_correct_a,(satz130 _ b1),<-satz131.
apply (@satz136b _ _ a2).
rewrite (satz131 (add_cut b1 _)),(satz130 (sub_cut _ _ _)),
sub_cut_correct_a,(satz130 _ a1).
rewrite <-satz131,(satz130 a2 b2),<-satz131.
reflexivity.
subst a. subst b. 
generalize (@satz135 _ _ a2 F); intros A. 
rewrite (satz130 (sub_cut a1 _ _)),sub_cut_correct_a in A.
generalize (@satz135 _ _ b1 A); intros B.
rewrite (satz130 (add_cut (sub_cut _ _ _) _)),<-satz131 in B.
rewrite sub_cut_correct_a,(satz130 _ a2) in B.
rewrite (str_equiv_c _ _ B).
reflexivity.
Qed.

Theorem satz185H3 {y:real} {a1 a2 b1 b2:cut} : 
   Z = a1 - a2 -> y = b1 - b2 -> Z + y = (a1 + b1) - (a2 + b2).
intros y a1 a2 b1 b2 A B. simpl in *.
destruct (str a1 a2) as [[E|E]|E]; try discriminate A.
subst a1.
destruct (str b1 b2) as [[F|F]|F].
generalize (@satz134 _ _ a2 F); intros C.
repeat rewrite (satz130 _ a2) in C.
rewrite (str_equiv_a _ _ C).
rewrite B.
apply (f_equal N).
apply (@satz136b _ _ (add_cut a2 b1)).
rewrite (satz130 (sub_cut _ _ C)),sub_cut_correct_a.
rewrite (satz130 _ (add_cut _ _)),satz131,sub_cut_correct_a.
reflexivity.
generalize (@satz134 _ _ a2 F); intros C.
repeat rewrite (satz130 _ a2) in C.
rewrite (str_equiv_b _ _ C).
rewrite B. apply (f_equal P).
apply (@satz136b _ _ (add_cut a2 b2)).
rewrite (satz130 (sub_cut _ _ C)),sub_cut_correct_a.
rewrite (satz130 _ (add_cut _ _)),satz131,sub_cut_correct_a.
reflexivity.
subst b1.
rewrite B.
rewrite (str_equiv_c _ _ (refl_equal (add_cut a2 b2))).
reflexivity.
Qed.

Theorem satz185 {x y:real} {a1 a2 b1 b2:cut} : 
   x = a1 - a2 -> y = b1 - b2 -> x + y = (a1 + b1) - (a2 + b2).
intros [|a|a] [|b|b] a1 a2 b1 b2 A B.
apply (satz185H3 A B).
apply (satz185H3 A B).
apply (satz185H3 A B).
generalize (satz185H3 B A); intros C.
rewrite (satz175 Z),(satz175 b1),(satz175 b2) in C.
apply C.
apply (satz185H1 A B).
apply (satz185H2 A B).
generalize (satz185H3 B A); intros C.
rewrite (satz175 Z),(satz175 b1),(satz175 b2) in C.
apply C.
generalize (satz185H2 B A); intros C.
rewrite (satz175 (P b)),(satz175 b1),(satz175 b2) in C.
apply C.
generalize (f_equal inv_add_real A); clear A; intros A.
generalize (f_equal inv_add_real B); clear B; intros B.
rewrite satz181 in A.
rewrite satz181 in B.
unfold inv_add_real in *.
generalize (satz185H1 A B); intros C.
rewrite <-(@satz177 (N a + N b)),satz180.
unfold inv_add_real.
rewrite C.
apply satz181.
Qed.

Theorem satz186 : associative real add_real.
intros x y z.
destruct (satz184 x) as [a1 [a2 A]].
destruct (satz184 y) as [b1 [b2 B]].
destruct (satz184 z) as [c1 [c2 C]].
generalize (satz185 A B); intros D.
generalize (satz185 D C); intros E.
rewrite E. clear D. clear E.
generalize (satz185 B C); intros D.
generalize (satz185 A D); intros E.
rewrite E. clear D. clear E.
simpl.
rewrite <-satz131,<-satz131.
reflexivity.
Qed.

Theorem add_real_identity_l : identity_l real Z add_real.
intros x. rewrite satz175. destruct x; tauto.
Qed.

Theorem sub_real_correct (x y:real) : x - y + y = x.
intros x y.
unfold sub_real.
rewrite satz186,satz179.
destruct x; reflexivity.
Qed.

Theorem satz187a {x y:real} : x + (y - x) = y.
intros x y.
unfold sub_real.
rewrite satz175,satz186,satz179.
destruct y; tauto.
Qed.

Theorem satz187b {x y:real} : exists z, x + z = y.
intros x y. exists (y-x).
apply satz187a.
Qed.

Theorem satz187c {x y v w:real} : x + v = y -> x + w = y -> v = w.
intros x y v w A B.
rewrite <-(add_real_identity_l v).
rewrite <-(@satz179 x),satz186,A.
rewrite <-B,<-satz186,satz179. apply add_real_identity_l.
Qed.

Theorem satz188a {x y z:real} : x < y -> x + z < y + z.
intros x y z A.
generalize (satz182d A); clear A; intros A.
unfold sub_real in A.
rewrite <-(add_real_identity_l y),(satz175 Z) in A.
rewrite <-(@satz179 z) in A.
rewrite (satz175 _ z),<-satz186,(satz186 (y+z)),<-satz180 in A.
rewrite (satz175 z x),(satz175 z),satz179 in A.
apply (satz182a A).
Qed.


Theorem satz188b {x y z:real} : x = y -> x + z = y + z.
intros x y z A. rewrite A. tauto.
Qed.

Theorem satz188c {x y z:real} : x + z < y + z -> x < y.
intros x y z A.
generalize (satz182d A); clear A; intros A.
unfold sub_real in A. rewrite satz180 in A.
rewrite (satz175 (inv_add_real x)) in A.
rewrite <-(satz186 (y+z)),(satz186 y),
(satz175 z),satz179,(satz175 _ Z),add_real_identity_l in A.
apply (satz182a A).
Qed.

Theorem satz188d {x y z:real} : x + z = y + z -> x = y.
intros x y z A.
generalize (satz182e A); clear A; intros A.
unfold sub_real in A. rewrite satz180 in A.
rewrite (satz175 (inv_add_real y)) in A.
rewrite <-(satz186 (x+z)),(satz186 x),
(satz175 z),satz179,(satz175 _ Z),add_real_identity_l in A.
apply (satz182b A).
Qed.

Theorem satz189 {x y z u:real} : x < y -> z < u -> x + z < y + u.
intros x y z u A B.
apply (satz171 _ (y+z)).
apply (satz188a A).
repeat rewrite (satz175 y).
apply (satz188a B).
Qed.

Theorem satz190a {x y z u:real} : x < y -> z <= u -> x + z < y + u.
intros x y z u A [B|B].
apply (satz189 A B).
subst z. apply (satz188a A).
Qed.

Theorem satz190b {x y z u:real} : x <= y -> z < u -> x + z < y + u.
intros x y z u [A|A] B.
apply (satz189 A B).
subst x; repeat rewrite (satz175 y).
apply (satz188a B).
Qed.

Theorem satz191 {x y z u:real} : x <= y -> z <= u -> x + z <= y + u.
intros x y z u [A|A] B.
left.
apply (satz190a A B).
destruct B as [B|B].
left.
apply satz190b. right. apply A.
apply B. subst x. subst z.
right. tauto.
Qed.


(** Multiplication of Reals *)

Definition mul_real (x y:real) := match x,y with
| Z, y => Z
| x, Z => Z
| P x, P y => P (x*y)
| N x, N y => P (x*y)
| P x, N y => N (x*y)
| N x, P y => N (x*y)
end.
Notation "x * y":=(mul_real x y).

Theorem satz192 {x y:real} : x * y = Z -> x = Z \/ y = Z.
intros [|a|a] [|b|b] A; try tauto; discriminate A.
Qed.

Theorem satz193 {x y:real} : abs_real (x * y) = abs_real x * abs_real y.
intros [|a|a] [|b|b]; tauto.
Qed.

Theorem satz194 : commutative real mul_real.
intros [|a|a] [|b|b]; try tauto;
unfold mul_real; rewrite (satz142); tauto.
Qed.

Theorem satz195 : identity_l real O mul_real.
intros [|a|a]; unfold mul_real,cut_to_real. tauto.
apply (f_equal P (satz151 a)).
apply (f_equal N (satz151 a)).
Qed.

Theorem satz196 {x y:real} : 
   x <> Z -> y <> Z -> x * y = abs_real x * abs_real y \/ x * y = inv_add_real (abs_real x * abs_real y).
intros [|a|a] [|b|b] A B; tauto.
Qed.

Theorem satz197a {x y:real} : inv_add_real x * y = x * inv_add_real y.
intros [|a|a] [|b|b]; tauto.
Qed.

Theorem satz197b {x y:real} : x * inv_add_real y = inv_add_real (x * y).
intros [|a|a] [|b|b]; tauto.
Qed.

Theorem satz198 {x y:real} : inv_add_real x * inv_add_real y = x * y.
intros [|a|a] [|b|b]; tauto.
Qed.

Theorem satz199 : associative real mul_real.
intros [|a|a] [|b|b] [|c|c]; try tauto; unfold mul_real; rewrite satz143; tauto.
Qed. 

Theorem satz200 {a b c:cut} : a * (b - c) = a * b - a * c.
intros a b c.
simpl.
destruct (str b c) as [[A|A]|A];
repeat (rewrite (satz142 a)).
rewrite (str_equiv_a _ _ (@satz145a _ _ a A)).
apply (f_equal N).
apply (@satz136b _ _ (mul_cut b a)).
repeat rewrite (satz130 _ (mul_cut b a)).
rewrite sub_cut_correct_a.
repeat rewrite (satz142 _ a).
rewrite <-satz144,sub_cut_correct_a. reflexivity.
rewrite (str_equiv_b _ _ (@satz145a _ _ a A)).
apply (f_equal P).
apply (@satz136b _ _ (mul_cut c a)).
rewrite (satz130 _ (mul_cut c a)),(satz130 _ (mul_cut c a)),
sub_cut_correct_a,(satz142 _ a),(satz142 _ a),(satz142 _ a).
rewrite <-satz144,sub_cut_correct_a.
reflexivity.
rewrite (str_equiv_c _ _ (satz145b A)).
tauto.
Qed.

Theorem satz201H0 (a b:cut) : @eq real (add_cut a b) (a+b).
intros a b; unfold cut_to_real,add_real; tauto.
Qed.

Theorem satz201H1 (a:cut) (y z:real) : a * (y + z) = a * y + a * z.
intros a y z.
destruct (satz184 y) as [b1 [b2 A]].
destruct (satz184 z) as [c1 [c2 B]].
generalize (satz185 A B); intros C.
set (u:=a*y+a*z); fold u.
rewrite C.
generalize (@satz200 a (add_cut b1 c1) (add_cut b2 c2)).
unfold cut_to_real,add_real.
intros E; rewrite E.
unfold mul_real.
rewrite satz144,satz144.
generalize (satz201H0 (mul_cut a b1) (mul_cut a c1)).
unfold cut_to_real; intros F; rewrite F.
generalize (satz201H0 (mul_cut a b2) (mul_cut a c2)).
unfold cut_to_real; intros G; rewrite G.
assert (D:u=a*y+a*z).
reflexivity.
rewrite A,B in D.
generalize (@satz200 a b1 b2); unfold cut_to_real; intros H.
unfold cut_to_real in D.
rewrite H in D.
generalize (@satz200 a c1 c2); unfold cut_to_real; intros J.
rewrite J in D.
set (v:=P a * P b1 - P a * P b2).
set (w:=P a * P c1 - P a * P c2).
assert (K:v=P a * P b1 - P a * P b2). reflexivity.
assert (L:w=P a * P c1 - P a * P c2). reflexivity.
generalize (satz185 K L); intros M.
unfold cut_to_real in M.
rewrite <-M,K,L,D.
reflexivity.
Qed.

Theorem satz201H2 (a:cut) (x:real) : N a * x = inv_add_real (P a * x).
intros a [|b|b]; tauto.
Qed.

Theorem satz201 : distributes real add_real mul_real.
intros [|a|a] y z.
reflexivity.
apply satz201H1.
rewrite satz201H2,satz201H2,satz201H2,<-satz180.
apply (f_equal inv_add_real).
generalize (satz201H1 a y z). intros A.
unfold cut_to_real in A. apply A.
Qed.

Theorem satz202 : distributes real sub_real mul_real.
intros x y z.
unfold sub_real.
rewrite <-satz197b.
apply satz201.
Qed.

Theorem satz203a (x y z:real) : x < y -> Z < z -> x * z < y * z.
intros [|a|a] [|b|b] [|c|c] A B; unfold mul_real,lt_real in *; try (simpl;tauto).
apply (satz145a A).
apply (satz145a A).
Qed.

Theorem satz203b (x y z:real) : x < y -> Z = z -> x * z = y * z.
intros [|a|a] [|b|b] z; intros A B; rewrite <-B; tauto.
Qed.

Theorem satz203c (x y z:real) : x < y -> z < Z -> y * z < x * z.
intros [|a|a] [|b|b] [|c|c] A B; unfold mul_real,lt_real in *; try (simpl;tauto).
apply (satz145a A).
apply (satz145a A).
Qed.

Theorem satz203d (x y z : real) : x * z < y * z -> Z < z -> x < y.
intros x y z A B.
destruct (satz167H0 x y) as [C|[C|C]].
apply C.
destruct (satz167H1 _ _ A).
rewrite C; tauto.
destruct (satz167H2 _ _ A (satz203a _ _ _ C B)).
Qed.

Definition neq_zero (x:real) := match x with
| Z => false
| _ => true
end.

Definition inv_mul_real (x:real) : neq_zero x -> real := match x with
| Z => fun (l:neq_zero Z) => match l with end
| P a => fun _ => P (inv_cut a)
| N a => fun _ => N (inv_cut a)
end.

Lemma inv_mul_real_correct (x:real) (l:neq_zero x): inv_mul_real x l * x = O.
intros [|a|a] A; try destruct A; unfold inv_mul_real,mul_real;
rewrite satz142; apply (f_equal P satz152a).
Qed.

Definition inv_mul_real' (x:real) : real := match x with
| Z => Z
| P a => P (inv_cut a)
| N a => N (inv_cut a)
end.

Lemma inv_mul_real_equiv (x:real) (l:neq_zero x) : inv_mul_real x l = inv_mul_real' x.
intros [|a|a]; try tauto.
intros [].
Qed.

Definition quotient_real (x y:real) (l:neq_zero y) := x * inv_mul_real y l.

Lemma quotient_real_correct (x y:real) (l:neq_zero y) : quotient_real x y l * y = x.
intros x y l.
unfold quotient_real.
rewrite satz199,inv_mul_real_correct,satz194.
apply satz195.
Qed.

Theorem satz204a (x y:real) (l:neq_zero y) : y * quotient_real x y l = x.
intros x y l.
rewrite satz194.
apply quotient_real_correct.
Qed.

Theorem satz204b (x y z:real) (l:neq_zero y): exists z, y * z = x.
intros x y z l.
exists (quotient_real x y l). apply satz204a.
Qed.

Theorem satz204c (x y v w:real) (l:neq_zero y) : y * v = x -> y * w = x -> v = w.
intros x y v w l A B.
rewrite <-B in A; clear B.
generalize (satz182e A); clear A; intros A.
rewrite <-satz202 in A. symmetry in A.
destruct (satz192 A) as [B|B]. subst y. destruct l.
symmetry in B.
apply (satz182b B).
Qed.

Lemma ninpl (x:real) : exists y, y < x.
intros x. exists (x-O).
apply satz182c.
unfold sub_real.
rewrite satz175,<-satz186.
rewrite satz179.
exact I.
Qed.

Lemma ninpr (x:real) : exists y, x < y.
intros x. exists (x+O).
apply satz182a.
unfold sub_real.
rewrite satz175,<-satz186,satz179.
exact I.
Qed.

Lemma tarski3 : dense real lt_real.
intros [|x|x] [|y|y] A; try (simpl in *;tauto).
destruct (p1 y) as [a B].
exists (P a). split. tauto.
apply (satz158a B).
destruct (dense_cut x y A) as [a [B C]].
exists (P a). tauto.
destruct (p1 x) as [a B].
exists (N a). split; try tauto.
simpl. apply (satz158a B).
exists Z. tauto.
destruct (dense_cut y x A) as [a [B C]].
exists (N a). tauto.
Qed.

Lemma tarski5 : ac_twist real add_real.
intros x y z. rewrite (satz175 y z),satz186.
reflexivity.
Qed.

Lemma tarski6 : exist_solns_1 real add_real.
intros x y.
exists (sub_real x y).
unfold sub_real.
rewrite <-satz186,satz175,<-satz186,satz179.
reflexivity.
Qed.

Lemma tarski7 : less_plus real add_real lt_real.
intros x y z u A.
destruct (@satz167H0 x y) as [B|[B|B]].
tauto.
subst x. right.
repeat rewrite (satz175 y _) in A.
apply (satz188c A).
right.
destruct (@satz167H0 z u) as [C|[C|C]].
apply C. subst z.
destruct (satz167H2 _ _ A (satz188a B)).
destruct (satz167H2 _ _ A (satz189 B C)).
Qed.

Lemma tarski8 : one_less_two real O add_real lt_real.
unfold cut_to_real,lt_real,add_real. apply satz133.
Qed.

(** Equivalences of strong trichotomy, strong xm *)


Lemma SXM_STR : SXM -> STR cut lt_cut.
intros sxm x y.
destruct (sxm (lt_cut x y)) as [A|A].
tauto.
destruct (sxm (lt_cut y x)) as [B|B].
tauto.
right.
generalize (@satz123H0 x y).
intros [C|[C|C]]; tauto.
Qed.

Lemma STR_SXM : STR cut lt_cut -> SXM.
intros stri x.
unfold STR in *.
destruct (stri (cp x) (cp (~x))) as [[A|A]|A].
right.
destruct A as [a [A B]].
unfold cp,pset in *;simpl in *.
case_eq (lt_prat a (S O)); intros C; rewrite C in *. tauto.
case_eq (lt_prat a (S(S O))); intros D; rewrite D in *. tauto.
tauto.
left.
destruct A as [a [A B]].
unfold cp,pset in *;simpl in *.
case_eq (lt_prat a (S O)); intros C; rewrite C in *. tauto.
case_eq (lt_prat a (S(S O))); intros D; rewrite D in *. tauto.
tauto.
generalize (cut_order_equiv_a A (S O)); intros B.
unfold eq_cut,cp,pset in B;simpl in *. tauto.
Qed.

Lemma SXM_XM : SXM -> XM.
intros sxm x.
destruct (sxm x); tauto.
Qed.