Library reals

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.