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

Definition p1_set {R:Type} (s:R->Prop) := exists x, s x.
Definition p2_set {R:Type} (s:R->Prop) := exists x, ~ s x.
Definition p3_set {R:Type} (s:R->Prop) (lt:R->R->bool) := forall x y, s y -> lt x y -> s x.
Definition p4_set {R:Type} (s:R->Prop) (lt:R->R->bool) := forall x, s x -> exists y, s y /\ lt x y.

Record cut := Cut
   {pcut : prat -> Prop;
    p1 : p1_set pcut;
    p2 : p2_set pcut;
    p3 : p3_set pcut lt_prat;
    p4 : p4_set pcut lt_prat}.

Definition CE : Prop := forall x y : cut, (forall a, pcut x a <-> pcut y a) -> x = y.

Variable ce : CE.

Variable xm : XM.

Lemma p3_equiv {pcut:prat->Prop} : p3_set pcut lt_prat -> forall a b, pcut a -> ~ pcut b -> a < b.
intros p A a b B C.
destruct (satz81H0 a b) as [D|[D|D]].
exact D.
subst a. destruct (C B).
destruct (C (A _ _ B D)).
Qed.

Definition eq_cut (x y:cut) := forall a, pcut x a <-> pcut y a.
Notation "x == y":=(eq_cut x y).

Theorem satz116 : reflexive cut eq_cut.
intros x a. tauto.
Qed.

Theorem satz117 : symmetric cut eq_cut.
intros x y A a. split; intros B.
apply (A _). exact B.
apply (A _). exact B.
Qed.

Theorem satz118 : transitive cut eq_cut.
intros x y z A B a. split; intros C.
apply (B _), (A _). exact C.
apply (A _), (B _). exact C.
Qed.

Lemma cut_order_equiv_a {x y:cut} : x = y -> x == y.
intros x y A. rewrite A.
apply satz116.
Qed.

Lemma cut_order_equiv_b {x y:cut} : x == y -> x = y.
apply ce.
Qed.

Theorem satz119 {x:cut} {a b:prat} : ~ pcut x a -> a < b -> ~ pcut x b.
intros [x x1 x2 x3 x4] a b A B C. simpl in *.
contradiction (A (x3 _ _ C B)).
Qed.

Definition lt_cut (x y:cut) := exists z, pcut y z /\ ~ pcut x z.
Notation "x < y":=(lt_cut x y).

Theorem satz123H0 : trichotomy cut lt_cut.
intros x y.
destruct (xm (lt_cut x y)) as [A|A].
tauto.
destruct (xm (lt_cut y x)) as [B|B].
tauto. right. left.
apply cut_order_equiv_b.
intros a. split; intros C.
destruct (xm (pcut y a)). apply H.
contradiction B. exists a. tauto.
destruct (xm (pcut x a)). apply H.
contradiction A. exists a. tauto.
Qed.

Theorem satz123H1 {x y:cut} : x < y -> x = y -> False.
intros x y [u [A B]] C.
rewrite <- C in A. destruct (B A).
Qed.

Theorem satz123H2 {x y:cut} : x < y -> y < x -> False.
intros [x x1 x2 x3 x4] [y y1 y2 y3 y4] [u [A B]] [v [C D]]. simpl in *.
contradiction (satz81H2 (p3_equiv y3 _ _ A D) (p3_equiv x3 _ _ C B)).
Qed.

Theorem satz123H3 {x y:cut} : y < x -> x = y -> False.
intros x y A B. symmetry in B.
apply (satz123H1 A B).
Qed.

Theorem satz126 : transitive cut lt_cut.
intros [x x1 x2 x3 x4] [y y1 y2 y3 y4] [z z1 z2 z3 z4] [a [A B]] [b [C D]].
unfold lt_cut in *.
exists b. split. apply C.
intros E.
apply (satz81H2 (p3_equiv y3 _ _ A D) (p3_equiv x3 _ _ E B)).
Qed.

Lemma lt_cut_irreflexive : irreflexive cut lt_cut.
intros x A. apply (satz123H2 A). tauto.
Qed.

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

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

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

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

Theorem leq_cut_reflexive : reflexive cut (fun x y => x <= y).
intros x. tauto.
Qed.

Definition add_set (p q : prat->Prop):= fun u:prat => exists x, exists y, p x /\ q y /\ u = x+y.

Lemma p1_add_proof {x y:cut} : p1_set (add_set (pcut x) (pcut y)).
intros [x [u A] x2 x3 x4] [y [v B] y2 y3 y4]. simpl.
exists (u+v).
unfold add_set. exists u. exists v.
split. apply A.
split. apply B.
reflexivity.
Qed.

Lemma p2_add_proof {x y:cut} : p2_set (add_set (pcut x) (pcut y)).
intros [x x1 [u A] x3 x4] [y y1 [v B] y3 y4]. simpl.
exists (u+v). unfold add_set.
intros [a [b [C [D E]]]].
contradiction (satz81H1 (satz98 (p3_equiv x3 _ _ C A) (p3_equiv y3 _ _ D B)) E).
Qed.

Lemma p3_add_proof {x y:cut} : p3_set (add_set (pcut x) (pcut y)) lt_prat.
intros [x x1 x2 x3 x4] [y y1 y2 y3 y4] a b [v [w [A [B C]]]] D.
exists (quotient_prat a (v+w) * v).
exists (quotient_prat a (v+w) * w). simpl in *.
split. apply (x3 _ v).
apply A.
rewrite C in D.
rewrite <- (@mul_prat_identity_l (v+w)) in D.
rewrite <-(@quotient_prat_correct_a a (v+w)) in D.
generalize (satz106a D); intros F.
generalize (@satz105a _ _ v F); intros G.
rewrite mul_prat_identity_l in G.
apply G.
split. apply (y3 _ w).
apply B.
rewrite C in D.
rewrite <- (@mul_prat_identity_l (v+w)) in D.
rewrite <-(@quotient_prat_correct_a a (v+w)) in D.
generalize (satz106a D); intros F.
generalize (@satz105a _ _ w F); intros G.
rewrite mul_prat_identity_l in G.
apply G.
rewrite <- satz104.
symmetry. apply quotient_prat_correct_a.
Qed.

Lemma p4_add_proof {x y:cut} : p4_set (add_set (pcut x) (pcut y)) lt_prat.
intros [x x1 x2 x3 x4] [y y1 y2 y3 y4] a [v [w [A [B C]]]]. simpl in *.
destruct (x4 _ A) as [r [D E]].
destruct (y4 _ B) as [s [F G]].
exists (r+s). split. exists r. exists s.
split. apply D. split. apply F. reflexivity.
rewrite C. apply (satz98 E G).
Qed.

Definition add_cut (x y:cut) := Cut (add_set (pcut x) (pcut y)) p1_add_proof p2_add_proof p3_add_proof p4_add_proof.
Notation "x + y":=(add_cut x y).

Theorem satz130 (x y:cut) : x + y = y + x.
intros [x x1 x2 x3 x4] [y y1 y2 y3 y4].
apply cut_order_equiv_b. unfold eq_cut. unfold add_cut. simpl.
intros a. split.
intros [v [w [A [B C]]]].
exists w. exists v. split. apply B. split. apply A. rewrite C. apply satz92.
intros [v [w [A [B C]]]].
exists w. exists v. split. apply B. split. apply A. rewrite C. apply satz92.
Qed.

Theorem satz131 (x y z:cut) : (x + y) + z = x + (y + z).
intros [x x1 x2 x3 x4] [y y1 y2 y3 y4] [z z1 z2 z3 z4].
apply cut_order_equiv_b. unfold eq_cut. unfold add_cut. simpl.
intros a. split.
intros [t [u [[v [w [A [B C]]]] [D E]]]].
exists v. exists (add_prat w u). split. apply A.
split. exists w. exists u. tauto.
subst t a. apply satz93.
intros [t [u [A [[v [w [B [C D]]]] E]]]].
exists (add_prat t v). exists w. split.
exists t. exists v. tauto.
split. apply C. subst u a. symmetry. apply satz93.
Qed.

Lemma satz132 (a:prat) (x:cut) : exists l, exists u, exists k, pcut x l /\ ~ pcut x u /\ sub_prat u l k = a.
intros a [x [b A] [c B] x3 x4].
destruct (@satz115 a c) as [n C].
generalize (@satz95 _ _ b C); intros D.
cut (lt_prat c (add_prat c b)). intros E.
generalize (satz86 c _ _ E D); intros F.
rewrite satz92 in F.
cut (~ x (add_prat b (mul_prat n a))). intros G.
destruct (@XM_WP xm (fun i => ~ x (add_prat b (mul_prat i a)))) as [u H].
exists n. apply G.
destruct u. exists b. exists (add_prat b a).
exists (satz94). simpl.
destruct H as [I J]. rewrite mul_prat_identity_l in I.
split. apply A.
split. apply I. apply (@satz97b _ _ b).
rewrite satz92,(sub_prat_correct_a). apply satz92.
exists (add_prat b (mul_prat u a)). exists (add_prat b (mul_prat (S u) a)).
simpl.
assert (L:lt_prat (add_prat b (mul_prat u a)) (add_prat b (mul_prat (S u) a))).
repeat rewrite (satz92 b _).
apply satz95.
apply satz105a. rewrite <-nat_to_prat_S.
apply satz94.
destruct H as [I J]. exists L. split.
destruct (xm (x (add_prat b (mul_prat u a)))) as [K|K].
apply K. contradiction (lt_nat_irreflexive (J _ K)).
split. apply I.
apply (@satz97b _ _ (add_prat b (mul_prat u a))).
rewrite satz92, sub_prat_correct_a.
rewrite <- nat_to_prat_S.
rewrite (satz102 _ a),satz104,(satz102 a O),mul_prat_identity_l.
rewrite <-satz93,(satz102 a u). apply satz92.
intros G. contradiction (B (x3 _ _ G F)).
apply satz94.
Qed.

Lemma satz133 {x y:cut} : x < x + y.
intros [x x1 x2 x3 x4] [y [a A] y2 y3 y4]. unfold lt_cut. simpl.
destruct (satz132 a (Cut x x1 x2 x3 x4)) as [l [u [K [B [C D]]]]].
simpl in *.
exists u; split.
exists l. exists a. rewrite satz92.
split. tauto. split. tauto.
rewrite <-D. rewrite satz92.
symmetry. apply sub_prat_correct_a.
apply C.
Qed.

Lemma satz134 {x y z:cut} : x < y -> x + z < y + z.
intros [x x1 x2 x3 x4] [y y1 y2 y3 y4] [z z1 z2 z3 z4] [u [A B]]. simpl in *.
destruct (y4 _ A) as [v [C D]].
destruct (@satz101a v u D) as [a E].
destruct (satz132 a (Cut z z1 z2 z3 z4)) as [b [c [K[F [G H]]]]]. simpl in *.
assert (I: add_prat u c = add_prat v b).
generalize (@satz96 _ _ b H); clear H; intros H.
rewrite satz92 in H.
rewrite sub_prat_correct_a in H.
subst c. subst v. symmetry. apply satz93.
exists (add_prat v b). simpl. split.
exists v. exists b. tauto.
rewrite <- I.
intros [d [e [J[M L]]]].
contradiction (satz81H1 (satz98 (p3_equiv x3 _ _ J B) (p3_equiv z3 _ _ M G)) L).
Qed.

Lemma satz135 {x y z:cut} : x = y -> x + z = y + z.
intros x y z A.
rewrite A. reflexivity.
Qed.

Lemma satz136a {x y z:cut} : x + z < y + z -> x < y.
intros x y z A.
destruct (@satz123H0 x y) as [B|[B|B]].
apply B.
contradiction (satz123H1 A (satz135 B)).
contradiction (satz123H2 A (satz134 B)).
Qed.

Lemma satz136b {x y z:cut} : x + z = y + z -> x = y.
intros x y z A.
destruct (@satz123H0 x y) as [B|[B|B]].
contradiction (satz123H1 (satz134 B) A).
apply B.
contradiction (satz123H3 (satz134 B) A).
Qed.

Lemma satz137 {x y z u:cut} : x < y -> z < u -> x + z < y + u.
intros x y z u A B.
apply (satz126 _ _ _ (satz134 A)).
repeat (rewrite (satz130 y _)).
apply (satz134 B).
Qed.

Lemma satz138a {x y z u:cut} : x < y -> z <= u -> x + z < y + u.
intros x y z u A [B|B].
apply (satz137 A B).
subst z. apply (satz134 A).
Qed.

Lemma satz138b {x y z u:cut} : x <= y -> z < u -> x + z < y + u.
intros x y z u [A|A] B.
apply (satz137 A B).
subst x.
repeat (rewrite (satz130 y)).
apply (satz134 B).
Qed.

Lemma satz139 {x y z u:cut} : x <= y -> z <= u -> x + z <= y + u.
intros x y z u [A|A] B.
left. apply (satz138a A B).
destruct B as [B|B].
left. apply satz138b. tauto. apply B.
right. rewrite A,B. reflexivity.
Qed.

Definition sub_cut_set (p q:prat->Prop) (a:prat) := exists b, exists c, exists l, p b /\ ~ q c /\ a = sub_prat b c l.

Lemma p1_sub_proof {x y:cut} {l:y<x} : p1_set (sub_cut_set (pcut x) (pcut y)).
intros x y [a [A B]].
destruct (p4 x a A) as [b [C E]].
exists (sub_prat b a E).
exists b. exists a. exists E.
tauto.
Qed.

Lemma p2_sub_proof {x y:cut} : p2_set (sub_cut_set (pcut x) (pcut y)).
intros x y.
destruct (p2 x) as [a A].
exists a. intros [b [c [K [B [C D]]]]].
cut (lt_prat a b). intros F.
apply (A (p3 x _ _ B F)).
rewrite D. apply (@satz97a _ _ c).
rewrite (satz92 (sub_prat b c K)).
rewrite sub_prat_correct_a.
apply satz94.
Qed.

Lemma p3_sub_proof {x y:cut} : p3_set (sub_cut_set (pcut x) (pcut y)) lt_prat.
intros x y a b [c [d [K [A [B C]]]]] D.
rewrite C in D.
generalize (@satz95 _ _ d D); intros E.
rewrite (satz92 (sub_prat c d K)) in E.
rewrite sub_prat_correct_a in E.
exists (add_prat a d). exists d.
rewrite (satz92 a d). exists satz94. split.
rewrite (satz92 d a). apply (p3 x _ _ A E).
split. apply B.
apply (@satz97b _ _ d).
rewrite (satz92 (sub_prat (add_prat d a) d satz94)).
rewrite sub_prat_correct_a. apply satz92.
Qed.

Lemma p4_sub_proof {x y:cut} : p4_set (sub_cut_set (pcut x) (pcut y)) lt_prat.
intros x y a [b [c [K [A [B C]]]]].
destruct (p4 x _ A) as [d [D E]].
generalize (satz86 _ _ _ K E); intros G.
generalize E; intros H.
rewrite <-(sub_prat_correct_a c b K) in E.
rewrite <-(sub_prat_correct_a _ _ G) in E.
repeat rewrite (satz92 c) in E.
generalize (satz97a E); intros J.
exists (sub_prat d c G). split.
exists d. exists c. exists G. tauto.
rewrite C. apply J.
Qed.

Definition sub_cut (x y:cut) (l:y<x) := Cut (sub_cut_set (pcut x) (pcut y)) (@p1_sub_proof _ _ l) p2_sub_proof p3_sub_proof p4_sub_proof.

Lemma satz140H0 {x y:cut} {a:prat} : x < y -> pcut x a -> pcut y a.
intros x y a [z [A B]] C.
apply (p3 y _ _ A (p3_equiv (p3 x) _ _ C B)).
Qed.

Lemma sub_cut_correct_a {x y:cut} {l:x < y} : x + (@sub_cut y x l) = y.
intros x y l; symmetry. apply ce.
intros a; split.
intros A. destruct (xm (pcut x a)) as [M|M].
apply (@satz140H0 x (x + sub_cut y x l)). apply satz133.
apply M.
destruct (p4 y _ A) as [u [D E]].
destruct (satz132 (sub_prat u a E) x) as [b [c [K [F [G H]]]]].
generalize (@satz96 _ _ b H); intros I.
rewrite (satz92 (sub_prat c b K)),sub_prat_correct_a in I.
generalize (p3_equiv (p3 x) _ _ F M); intros J.
generalize (@satz96 _ _ (sub_prat a b J) I); intros L.
cut (lt_prat c u). intros O.
rewrite satz93,(sub_prat_correct_a _ _ J),
(satz92 _ a),(sub_prat_correct_a _ _ E),<-(sub_prat_correct_a c u O) in L.
repeat rewrite (satz92 c) in L.
generalize (satz97b L); clear L; intros L.
generalize (@satz96 _ _ b L); intros N.
rewrite (satz92 (sub_prat a b J)),(sub_prat_correct_a _ _ J) in N.
exists b. exists (sub_prat u c O). split.
apply F. split.
exists u. exists c. exists O. tauto.
rewrite N. apply satz92.
rewrite I. apply (@satz97a _ _ a).
rewrite satz93,(satz92 b a),<-satz93,(satz92 _ a),(sub_prat_correct_a _ _ E).
repeat rewrite (satz92 u _). apply (satz95 J).
intros [b [c [A [[d [e [K [B [C D]]]]] E]]]].
rewrite D in E.
generalize (p3_equiv (p3 x) _ _ A C); intros F.
cut (lt_prat (add_prat (sub_prat d e K) b) d).
intros G. rewrite E.
rewrite satz92 in G.
apply (p3 y _ _ B G).
cut (add_prat (add_prat (sub_prat d e K) b) (sub_prat e b F) = d).
intros H. apply (@satz97a _ _ (sub_prat e b F)). rewrite H. apply satz94.
rewrite satz93,(sub_prat_correct_a _ _ F),satz92. apply (sub_prat_correct_a _ _ K).
Qed.

Lemma satz140b {x y:cut} : x < y -> exists z, x + z = y.
intros x y l. exists (sub_cut y x l).
apply sub_cut_correct_a.
Qed.

Lemma sub_cut_PI {x y:cut} {m n:lt_cut y x} : sub_cut x y m = sub_cut x y n.
intros x y m n. apply ce.
unfold sub_cut. simpl. tauto.
Qed.

Definition mul_set (p q : prat->Prop):= fun u:prat => exists x, exists y, p x /\ q y /\ u = x*y.

Lemma p1_mul_proof {x y:cut} : p1_set (mul_set (pcut x) (pcut y)).
intros [x [u A] x2 x3 x4] [y [v B] y2 y3 y4]. simpl.
exists (u*v).
unfold mul_set. exists u. exists v.
split. apply A.
split. apply B.
reflexivity.
Qed.

Lemma p2_mul_proof {x y:cut} : p2_set (mul_set (pcut x) (pcut y)).
intros [x x1 [u A] x3 x4] [y y1 [v B] y3 y4]. simpl.
exists (u*v). unfold mul_set.
intros [a [b [C [D E]]]].
contradiction (satz81H1 (satz107 (p3_equiv x3 _ _ C A) (p3_equiv y3 _ _ D B)) E).
Qed.

Lemma p3_mul_proof {x y:cut} : forall a b, mul_set (pcut x) (pcut y) b -> lt_prat a b -> mul_set (pcut x) (pcut y) a.
intros [x x1 x2 x3 x4] [y y1 y2 y3 y4] a b [v [w [A [B C]]]] D. simpl in *.
rewrite C in D.
cut (mul_prat v (quotient_prat a v) = a). intros E.
cut (lt_prat (quotient_prat a v) w). intros F.
exists v. exists (quotient_prat a v). split. apply A.
split. apply (y3 _ _ B F). symmetry. apply E.
rewrite<- (mul_prat_identity_l w).
rewrite <-(@quotient_prat_correct_a O v).
rewrite satz103.
rewrite quotient_prat_correct_b. repeat (rewrite (satz102 (quotient_prat O v))).
apply (satz105a D).
symmetry. rewrite satz102.
symmetry. apply quotient_prat_correct_a.
Qed.

Lemma p4_mul_proof {x y:cut} : forall a, mul_set (pcut x) (pcut y) a -> exists b, mul_set (pcut x) (pcut y) b /\ lt_prat a b.
intros [x x1 x2 x3 x4] [y y1 y2 y3 y4] a [v [w [A [B C]]]]. simpl in *.
destruct (x4 _ A) as [l [D E]].
exists (mul_prat l w).
split. exists l. exists w. tauto.
rewrite C. apply (satz105a E).
Qed.

Definition mul_cut (x y:cut) := Cut (mul_set (pcut x) (pcut y)) p1_mul_proof p2_mul_proof p3_mul_proof p4_mul_proof.
Notation "x * y":=(mul_cut x y).

Theorem satz142 : commutative cut mul_cut.
intros [x x1 x2 x3 x4] [y y1 y2 y3 y4]. apply cut_order_equiv_b.
unfold eq_cut. intros a; split; intros [b [c [A [B C]]]]; simpl in *.
exists c. exists b. rewrite C. rewrite satz102. tauto.
exists c. exists b. rewrite C. rewrite satz102. tauto.
Qed.

Theorem satz143 : associative cut mul_cut.
intros [x x1 x2 x3 x4] [y y1 y2 y3 y4] [z z1 z2 z3 z4]. apply cut_order_equiv_b.
unfold eq_cut. intros a; split; intros [b [c [A [C D]]]]; simpl in *.
destruct A as [d [e [E [F G]]]].
exists d. exists (mul_prat e c). split. apply E. split.
exists e. exists c. tauto. rewrite D,G. apply satz103.
destruct C as [d [e [E [F G]]]].
exists (mul_prat b d). exists e. split. exists b. exists d. tauto.
rewrite D,G. rewrite satz103. tauto.
Qed.

Theorem satz144 : distributes cut add_cut mul_cut.
intros [x x1 x2 x3 x4] [y y1 y2 y3 y4] [z z1 z2 z3 z4]. apply cut_order_equiv_b.
unfold eq_cut. simpl in *. intros a; split. intros [b [c [A [[d [e [B [C D]]]] E]]]].
exists (mul_prat b d). exists (mul_prat b e). split.
exists b. exists d. tauto. split.
exists b. exists e. tauto. rewrite E,D. apply satz104.
intros [b [c [[d [e [A [B C]]]] [[f [g [E [F G]]]] H]]]].
destruct (@satz81H0 d f) as [J|[J|J]].
destruct (satz101a J) as [h K].
symmetry in K. rewrite K in G.
apply (@p3_mul_proof (Cut x x1 x2 x3 x4) (Cut y y1 y2 y3 y4 + Cut z z1 z2 z3 z4) _ (add_prat a (mul_prat h e))). simpl.
exists f. exists (add_prat e g). split. apply E. split.
exists e. exists g. tauto.
rewrite H,C,G,K. rewrite satz104, (satz102 (add_prat d h) e), (satz102 _ g), satz104, satz104.
rewrite (satz102 e d),(satz102 e h),(satz93 (mul_prat d e)), (satz92 _ (mul_prat h e)), <-(satz93).
reflexivity. apply satz94.
subst d.
exists f. exists (add_prat e g). split. apply E. split.
exists e. exists g. tauto.
rewrite H,C,G. symmetry. apply satz104.
destruct (satz101a J) as [h K].
symmetry in K. rewrite K in C.
apply (@p3_mul_proof (Cut x x1 x2 x3 x4) (Cut y y1 y2 y3 y4 + Cut z z1 z2 z3 z4) _ (add_prat a (mul_prat h g))). simpl.
exists d. exists (add_prat e g). split. apply A. split.
exists e. exists g. tauto.
rewrite H,C,G,K. rewrite satz104,(satz102 (add_prat f h) g),(satz104).
repeat (rewrite (satz102 _ g)). apply satz93. apply satz94.
Qed.

Theorem satz145a {x y z:cut} : x < y -> x * z < y * z.
intros x y z A.
destruct (satz140b A) as [a B].
rewrite <-B. rewrite (satz142 (x+a)),(satz144),(satz142). apply satz133.
Qed.

Theorem satz145b {x y z:cut} : x = y -> x * z = y * z.
intros x y z A. rewrite A. reflexivity.
Qed.

Theorem satz146a {x y z:cut} : x * z < y * z -> x < y.
intros x y z A. destruct (@satz123H0 x y) as [B|[B|B]].
apply B.
contradiction (satz123H1 A (satz145b B)).
contradiction (satz123H2 A (satz145a B)).
Qed.

Theorem satz146b {x y z:cut} : x * z = y * z -> x = y.
intros x y z A. destruct (@satz123H0 x y) as [B|[B|B]].
contradiction (satz123H1 (satz145a B) A).
apply B.
contradiction (satz123H3 (satz145a B) A).
Qed.

Theorem satz147 {x y z u:cut} : x < y -> z < u -> x * z < y * u.
intros x y z u A B.
apply (satz126 _ (x*u)). repeat (rewrite (satz142 x)). apply (satz145a B).
apply (satz145a A).
Qed.

Theorem satz148a {x y z u:cut} : x <= y -> z < u -> x * z < y * u.
intros x y z u [A|A] B.
apply (satz147 A B). rewrite A,(satz142 y),(satz142 y).
apply (satz145a B).
Qed.

Theorem satz148b {x y z u:cut} : x < y -> z <= u -> x * z < y * u.
intros x y z u A [B|B].
apply (satz147 A B).
rewrite B. apply (satz145a A).
Qed.

Theorem satz149 {x y z u:cut} : x <= y -> z <= u -> x * z <= y * u.
intros x y z u [A|A] B. left.
apply (satz148b A B).
destruct B as [B|B].
left. apply satz148a. right. apply A. apply B.
right. rewrite A,B. reflexivity.
Qed.

Definition prat_cut_set (a:prat) := fun b => lt_prat b a.

Lemma p1_prat_cut_proof {a:prat} : exists b, prat_cut_set a b.
exact @satz90.
Qed.

Lemma p2_prat_cut_proof {a:prat} : exists b, ~ prat_cut_set a b.
intros a. destruct (@satz89 a) as [b A].
exists b. intros B. exact (satz81H2 A B).
Qed.

Lemma p3_prat_cut_proof {a:prat} : forall x y, prat_cut_set a y -> lt_prat x y -> prat_cut_set a x.
intros a x y A B.
apply (satz86 _ _ _ B A).
Qed.

Lemma p4_prat_cut_proof {a:prat} : forall x, prat_cut_set a x -> exists y, prat_cut_set a y /\ lt_prat x y.
intros a x A. unfold prat_cut_set. destruct (satz91 A) as [y [B C]].
exists y. split. apply C. apply B.
Qed.

Definition prat_to_cut (a:prat) := Cut (prat_cut_set a) p1_prat_cut_proof p2_prat_cut_proof p3_prat_cut_proof p4_prat_cut_proof.

Coercion prat_to_cut : prat >-> cut.

Definition is_rational_cut (x:cut) := exists a:prat, x = a.

Definition is_irrational_cut (x:cut) := ~ is_rational_cut x.

Theorem satz151 : identity_l cut O mul_cut.
intros [x x1 x2 x3 x4]. unfold mul_cut. simpl.
unfold prat_cut_set. unfold mul_set. apply cut_order_equiv_b. unfold eq_cut. simpl. split.
intros [b [c [A [B C]]]]. rewrite C. apply (x3 _ _ B).
generalize (@satz105a b O c A); intros D. rewrite mul_prat_identity_l in D. apply D.
intros A. destruct (x4 _ A) as [b [B C]].
exists (mul_prat (quotient_prat O b) a). exists b. split.
rewrite satz102.
generalize (@satz105a _ _ (quotient_prat O b) C); intros D.
rewrite (satz102 b) in D. rewrite quotient_prat_correct_a in D.
apply D.
split. apply B. rewrite satz102,<-satz103,(satz102 b).
rewrite quotient_prat_correct_a. symmetry.
apply mul_prat_identity_l.
Qed.

Definition inv_set (q:prat->Prop) (a:prat) := exists b, ~ q b /\ lt_prat b (inv_mul_prat a).

Lemma p1_inv_proof {x:cut} : p1_set (inv_set (pcut x)).
intros x.
destruct (p2 x) as [a A].
exists (inv_mul_prat (add_prat a a)).
exists a. split.
apply A.
rewrite inv_mul_prat_correct_b.
apply satz94.
Qed.

Lemma p2_inv_proof {x:cut} : p2_set (inv_set (pcut x)).
intros x.
destruct (p1 x) as [a A].
exists (inv_mul_prat a).
intros [b [B C]].
rewrite inv_mul_prat_correct_b in C.
apply B.
apply (p3 x b a A).
apply C.
Qed.

Lemma p3_inv_proof {x:cut} : p3_set (inv_set (pcut x)) lt_prat.
intros x a b [c [A B]] C.
generalize (@satz105a _ _ (inv_mul_prat b) C); intros D.
rewrite (satz102 b),inv_mul_prat_correct_a in D.
rewrite <-(inv_mul_prat_correct_a a),satz102 in D.
generalize (satz106a D); clear D; intros D.
exists (inv_mul_prat b).
split.
intros E.
apply A, (p3 x c _ E B).
apply D.
Qed.

Lemma p4_inv_proof {x:cut} : p4_set (inv_set (pcut x)) lt_prat.
intros x a [b [A B]].
destruct (satz91 B) as [d [E F]].
exists (inv_mul_prat d). split.
exists b. split. apply A.
rewrite inv_mul_prat_correct_b.
apply E.
rewrite <-(inv_mul_prat_correct_b a).
apply (inv_mul_prat_correct_c _ _ F).
Qed.

Definition inv_cut (x:cut) := Cut (inv_set (pcut x)) p1_inv_proof p2_inv_proof p3_inv_proof p4_inv_proof.

Theorem satz152a {x:cut} : x * inv_cut x = O.
intros x. apply ce.
intros a. split.
intros [b [c [A [[d [B C]] D]]]].
rewrite <-(inv_mul_prat_correct_a c),D.
simpl. apply satz105a.
apply (satz86 _ _ _ (p3_equiv (p3 x) _ _ A B) C).
intros A.
destruct (p1 x) as [b B].
destruct (satz132 (mul_prat (sub_prat O a A) b) x) as [l [u [K [C [D E]]]]].
generalize (p3_equiv (p3 x) _ _ B D); intros F.
generalize (@satz105a _ _ (sub_prat O a A) F); clear F; intros F.
rewrite (satz102 b),<-E,(satz102 u) in F.
generalize (@satz95 _ _ (mul_prat a u) F); clear F; intros F.
rewrite (satz102 _ u),(satz102 (sub_prat O a A)),<-satz104 in F.
unfold pcut,prat_to_cut,prat_cut_set in A.
rewrite (satz92 _ a),(sub_prat_correct_a _ _ A) in F.
rewrite (satz102 _ O),mul_prat_identity_l in F.
rewrite (satz92 (sub_prat u l K)) in F.
assert (G:(lt_prat (add_prat (mul_prat u a) (sub_prat u l K)) (add_prat l (sub_prat u l K)))).
rewrite sub_prat_correct_a. apply F.
generalize (satz97a G); clear F; clear G; intros F.
cut (lt_prat u (quotient_prat l a)). intros G.
exists l. exists (inv_mul_prat (quotient_prat l a)). split.
apply C. split.
exists u. split.
apply D. rewrite inv_mul_prat_correct_b. apply G.
apply (@satz106b _ _ (quotient_prat l a)).
rewrite (satz102 a),quotient_prat_correct_a,satz103.
rewrite inv_mul_prat_correct_a. symmetry. rewrite satz102.
apply mul_prat_identity_l.
apply (@satz106a _ _ a).
rewrite quotient_prat_correct_a.
apply F.
Qed.

Theorem satz152b {x:cut} : exists y, x * y = O.
intros x. exists (inv_cut x).
apply satz152a.
Qed.

Definition quotient_cut (x y:cut) := x * inv_cut y.

Theorem satz153a {x y:cut} : x * quotient_cut y x = y.
intros x y. unfold quotient_cut.
rewrite (satz142 y),<-satz143,<-satz151,satz152a.
reflexivity.
Qed.

Theorem satz153b {x y:cut} : exists z, x * z = y.
intros x y. exists (quotient_cut y x).
apply satz153a.
Qed.

Theorem satz153c {x y u v} : x * u = y -> x * v = y -> u = v.
intros x y u v A B.
rewrite <-A in B. rewrite (satz142 x),(satz142 x) in B.
symmetry. apply (satz146b B).
Qed.

Theorem satz154a {x y:prat} : lt_prat x y -> x < y.
intros x y A.
exists x. unfold prat_to_cut,pcut. split.
apply A.
unfold prat_cut_set. generalize (lt_prat_irreflexive x).
tauto.
Qed.

Theorem satz154b {x y:prat} : x < y -> lt_prat x y.
intros x y [a [A B]]. unfold prat_to_cut,pcut,prat_cut_set in *.
destruct (@satz81H0 x y) as [H|[H|H]].
apply H.
subst x. destruct (B A).
destruct (B (satz86 _ _ _ A H)).
Qed.

Theorem satz154c {x y:prat} : x = y -> @eq cut x y.
intros x y A. rewrite A. reflexivity.
Qed.

Theorem satz154d {x y:prat} : @eq cut x y -> x = y.
intros x y A.
destruct (@satz81H0 x y) as [B|[B|B]].
contradiction (satz123H1 (satz154a B) A).
apply B.
contradiction (satz123H3 (satz154a B) A).
Qed.

Theorem satz155a {x y:prat} : @eq cut (add_prat x y) (x + y).
intros x y. apply ce.
intros a. split.
unfold add_cut,prat_to_cut,add_set,prat_cut_set,pcut.
intros A. rewrite <-(mul_prat_identity_l (add_prat x y)),
<-(quotient_prat_correct_a _ (add_prat x y)) in A.
generalize (@satz106a _ _ _ A); clear A; intros A.
exists (mul_prat x (quotient_prat a (add_prat x y))).
exists (mul_prat y (quotient_prat a (add_prat x y))). split.
generalize (@satz105a _ _ x A); intros B.
rewrite mul_prat_identity_l,satz102 in B. apply B. split.
generalize (@satz105a _ _ y A); intros B.
rewrite mul_prat_identity_l,satz102 in B. apply B.
rewrite (satz102 x),(satz102 y),<-satz104,satz102.
rewrite satz102. symmetry. apply quotient_prat_correct_a.
unfold add_cut,prat_to_cut,add_set,prat_cut_set,pcut.
intros [b [c [A [B C]]]].
rewrite C.
apply (satz98 A B).
Qed.

Theorem satz155b {x y:prat} {k:lt_prat y x} {l: y < x} : @eq cut (sub_prat x y k) (@sub_cut x y l).
intros x y k l.
generalize (@satz155a (sub_prat x y k) y); intros A.
rewrite satz92,(sub_prat_correct_a _ _ k) in A.
rewrite <-(@sub_cut_correct_a y x l),satz130 in A.
symmetry. apply (satz136b A).
Qed.

Theorem satz155c {x y:prat} : @eq cut (mul_prat x y) (x * y).
intros x y; apply ce; intros a. split.
intros A.
destruct (satz91 A) as [b [B C]].
rewrite <-(mul_prat_identity_l b),<-(quotient_prat_correct_a a b) in B.
generalize (satz106a B); intros D.
generalize (@satz105a _ _ y D); clear D; intros D.
rewrite mul_prat_identity_l in D.
rewrite <-(quotient_prat_correct_a b y) in C.
generalize (satz106a C); intros E.
exists (quotient_prat b y). exists (mul_prat y (quotient_prat a b)).
split. apply E. split. rewrite satz102 in D.
apply D. rewrite <-satz103,quotient_prat_correct_a.
rewrite satz102. symmetry. apply quotient_prat_correct_a.
intros [b [c [A [B C]]]].
rewrite C. apply (satz107 A B).
Qed.

Theorem satz155d {x y:prat} : @eq cut (quotient_prat x y) (quotient_cut x y).
intros x y.
apply (@satz146b _ _ y).
rewrite <-satz155c. rewrite quotient_prat_correct_a.
rewrite satz142,satz153a. reflexivity.
Qed.

Theorem satz158a {x:cut} {a:prat} : pcut x a -> a < x.
intros x a. intros A.
exists a. split. apply A.
intros B.
destruct (lt_prat_irreflexive _ B).
Qed.

Theorem satz158b {x:cut} {a:prat} : a < x -> pcut x a.
intros x a. intros [b [A B]].
destruct (@satz81H0 a b) as [H|[H|H]].
apply (p3 x _ _ A H).
rewrite H. apply A.
destruct (B H).
Qed.

Theorem satz158c {x:cut} {a:prat} : ~ pcut x a -> x <= a.
intros x a A.
destruct (@satz123H0 x a) as [B|[B|B]]; try tauto.
destruct (A (satz158b B)).
Qed.

Theorem satz158d {x:cut} {a:prat} : x <= a -> ~ pcut x a.
intros x a [A|A] B.
destruct (satz123H2 A (satz158a B)).
destruct (satz123H3 (satz158a B) A).
Qed.

Definition lub (x:cut) (m:prat) := forall a, pcut x a <-> lt_prat a m.

Definition lub' (x:cut) (m:prat) := ~ pcut x m /\ forall a, ~ pcut x a -> leq_prat m a.

Lemma lub_equiv (x:cut) (m:prat) : lub x m <-> lub' x m.
intros x m. apply conj.
intros A. apply conj.
intros B.
destruct (A m) as [C _].
apply (satz81H1 (C B) (refl_equal _)).
intros a B.
destruct (A a) as [C D].
apply frac_order_equiv_d.
destruct (@satz81H0 a m) as [E|[E|E]].
destruct (B (D E)).
left. rewrite E. apply satz37.
right. apply E.
intros [A B] a.
apply conj.
intros C.
apply satz154b.
apply (satz127b (satz158a C) (satz158c A)).
intros C.
destruct (xm (pcut x a)).
apply H.
destruct (frac_order_equiv_c (B a H)) as [D|D].
destruct (satz81H1 C).
apply (eq_prat_equiv_f D).
destruct (satz81H2 C D).
Qed.

Theorem satz157a {x:prat} : lub x x.
intros x a.
tauto.
Qed.

Theorem satz157b {x:prat} : exists m, lub x m.
intros x. exists x. apply satz157a.
Qed.

Theorem satz157c {x:cut} {a:prat} : lub x a -> x = a.
intros x a.
exact (ce x a).
Qed.

Theorem satz157d {x:cut} : (exists m, lub x m) -> exists a : prat, x = a.
intros x [m A]. exists m.
apply (satz157c A).
Qed.

Theorem satz159 {x y:cut} : x < y -> exists a : prat, x < a /\ a < y.
intros x y [a [A B]].
destruct (p4 y _ A) as [b [C D]].
exists b. split. apply (@satz127a _ a).
destruct (@satz123H0 x a) as [H|[H|H]].
left. apply H.
right. apply H.
destruct (B (satz158b H)).
apply (satz154a D).
apply (satz158a C).
Qed.

Lemma ex_min_cut (x y:cut) : exists z, z<=x /\ z<=y.
intros x y. destruct (@satz123H0 x y) as [A|[A|A]].
exists x. tauto.
exists x. tauto.
exists y. tauto.
Qed.

Theorem satz160 {x y:cut} {a:prat} : x * y < a -> exists b:prat, exists c:prat, @eq cut a (b * c) /\ x <= b /\ y <= c.
intros x y a A.
destruct (ex_min_cut O (quotient_cut (sub_cut a (x * y) A) (x + y + O))) as [d [B1 B2]].
destruct (@satz159 x (x+d) satz133) as [b [C D]].
destruct (@satz159 y (y+d) satz133) as [c [E F]].
generalize (satz147 D F); clear D; clear F; intros G.
rewrite satz144,(satz142 _ y) in G.
rewrite satz144,(satz142 y),(satz142 y) in G.
rewrite satz131,(satz142 _ d),<-satz144,<-satz131,(satz130 y x) in G.
generalize (@satz149 _ _ (x+y+O) (x+y+O) B2 (leq_cut_reflexive _));
intros H.
rewrite (satz142 (quotient_cut _ _) (x+y+O)),satz153a in H.
generalize (@satz149 d _ _ _ (leq_cut_reflexive _)
 (@satz139 (x+y) _ _ _ (leq_cut_reflexive _) B1)).
intros K.
generalize (@satz127b _ _ _ G (@satz139 (x*y) _ _ _
 (leq_cut_reflexive _) K)); clear G; clear K; intros G.
generalize (satz127b G (@satz139 (x*y) (x*y)_ _
 (leq_cut_reflexive _) H)); clear G; clear H; intros G.
rewrite sub_cut_correct_a in G.
exists (quotient_prat a c). exists c.
split. symmetry. rewrite satz142,satz155d. apply satz153a.
split. left. apply (satz126 _ _ _ C).
apply (@satz146a _ _ c).
rewrite (satz142 (quotient_prat a c)).
rewrite satz155d,(satz153a). apply G.
left. apply E.
Qed.

Definition sqrt_set (x:cut) (a:prat) := a * a < x.

Lemma p1_sqrt_proof (x:cut) : p1_set (sqrt_set x).
intros x.
destruct (@satz123H0 O x) as [A|[A|A]].
exists O. unfold sqrt_set. rewrite satz151. apply A.
exists (O/(S O)).
rewrite <-(satz151 x).
rewrite <-A.
apply satz147; apply satz158a; exact I.
destruct (p1 x) as [a B].
exists a.
rewrite <-(satz151 x).
apply (satz147 (satz126 _ _ _ (satz158a B) A) (satz158a B)).
Qed.

Lemma p2_sqrt_proof (x:cut) : p2_set (sqrt_set x).
intros x. rewrite <-(satz151 x).
destruct (@satz123H0 O x) as [A|[A|A]].
destruct (p2 x) as [a B].
exists a. unfold sqrt_set.
intros C. rewrite (satz151 x) in C.
cut (a < a * a). intros D.
apply B. apply satz158b. apply (satz126 _ _ _ D C).
cut (pcut x O). intros D.
generalize (p3_equiv (p3 x) _ _ D B).
intros E. generalize (@satz105a _ _ a E).
rewrite mul_prat_identity_l.
intros F. rewrite <-satz155c. apply (satz154a F).
apply (satz158b A).
rewrite <-A.
exists O.
exact (lt_cut_irreflexive _).
exists O. unfold sqrt_set.
repeat rewrite (satz151 _).
intros B. contradiction (satz123H2 A B).
Qed.

Lemma p3_sqrt_proof (x:cut) : p3_set (sqrt_set x) lt_prat.
intros x a b A B. unfold sqrt_set in *.
apply (satz126 _ (b*b)).
apply (satz147 (satz154a B) (satz154a B)).
apply A.
Qed.

Lemma ex_less_cut (x y:cut) : exists z:prat, z<x /\ z<y.
intros x y.
destruct (ex_min_cut x y) as [z [A B]].
destruct (p1 z) as [a C].
exists a. split.
exists a. split.
apply satz158b.
apply (satz127b (satz158a C) A).
intros D; apply (lt_prat_irreflexive _ D).
exists a. split.
apply satz158b.
apply (satz127b (satz158a C) B).
intros D; apply (lt_prat_irreflexive _ D).
Qed.

Lemma p4_sqrt_proof (x:cut) : p4_set (sqrt_set x) lt_prat.
intros x a A.
destruct (ex_less_cut O (quotient_cut (sub_cut x (a*a) A) (a+(a+O)))) as [b [B1 B2]].
cut ((a+b)*(a+b)<x).
intros C. exists (add_prat a b).
split. unfold sqrt_set.
rewrite satz155a. apply C.
apply satz94.
rewrite satz144,(satz142 _ a),satz144.
rewrite <-(@sub_cut_correct_a _ x A).
apply (satz126 _ (a*a+(a+(a+O))*b)).
rewrite (satz142 (add_cut _ (add_cut _ _)) b),satz144,<-satz131.
rewrite (satz142 b a),(satz130 (a*a+a*b)),(satz130 (a*a+a*b)).
apply satz134.
rewrite (satz142 b).
apply satz145a.
rewrite (satz130 a),(satz130 a).
apply (satz134 B1).
generalize (@satz145a _ _ (a+(a+O)) B2).
rewrite (satz142 b),(satz142 _ (a+(a+O))),satz153a.
intros C.
repeat rewrite (satz130 (a*a)).
apply (satz134 C).
Qed.

Definition sqrt_cut (x:cut) := Cut (sqrt_set x) (p1_sqrt_proof x) (p2_sqrt_proof x) (p3_sqrt_proof x) (p4_sqrt_proof x).

Theorem satz161a {x:cut} : sqrt_cut x * sqrt_cut x = x.
intros x.
destruct (@satz123H0 (sqrt_cut x * sqrt_cut x) x) as [A|[A|[a [[b [c [A [B C]]]] D]]]].
destruct (satz159 A) as [a [B C]].
destruct (satz160 B) as [b [c [D [E F]]]].
destruct (@satz81H0 b c) as [G|[G|G]].
destruct (satz158d E).
unfold sqrt_cut. apply (satz126 _ a). rewrite D.
rewrite (satz142 b c). apply (satz145a (satz154a G)).
apply C.
subst b.
destruct (satz158d F).
rewrite D in C. apply C.
destruct (satz158d F).
unfold sqrt_cut.
apply (satz126 _ a). rewrite D.
apply (satz145a (satz154a G)).
apply C.
apply A.
simpl in *.
destruct D.
unfold sqrt_cut,sqrt_set in *.
destruct (@satz81H0 b c) as [E|[E|E]].
rewrite C. rewrite <-satz155c in B.
apply satz158b. exact (satz126 _ _ _ (satz154a (@satz105a _ _ c E)) B).
subst b.
rewrite <-satz155c,<-C in A.
apply (satz158b A).
rewrite <-satz155c in A.
rewrite C,satz102.
apply satz158b.
exact (satz126 _ _ _ (satz154a (@satz105a _ _ b E)) A).
Qed.

Theorem satz161b {y:cut} : exists x, x*x = y.
intros y. exists (sqrt_cut y).
apply satz161a.
Qed.

Theorem satz161c {v w y:cut} : v * v = y -> w * w = y -> v = w.
intros v w y A B.
rewrite <-B in A.
destruct (@satz123H0 v w) as [C|[C|C]].
contradiction (satz123H1 (satz147 C C) A).
apply C.
contradiction (satz123H3 (satz147 C C) A).
Qed.

Lemma satz162H0 {x y z u:cut} : x = y -> z = u -> x * z = y * u.
intros x y z u A B.
rewrite A,B.
reflexivity.
Qed.

Lemma satz162H1 {x y:nat} : leq_nat (S (mul_nat x x)) (mul_nat y y) -> leq_nat (S x) y.
intros x y A.
destruct (satz10H0 x y) as [B|[B|B]].
apply B.
subst x. destruct (lt_nat_irreflexive A).
destruct (satz10H2 _ _ A (satz34 B B)).
Qed.

Theorem satz162 : exists x, is_irrational_cut x.
exists (sqrt_cut (S O)).
intros [[[a1 a2] arp] A].
generalize (satz162H0 A A); clear A; intros A.
rewrite satz161a in A.
rewrite <-satz155c in A.
unfold mul_prat,rep,mul_frac in A.
generalize (eq_prat_equiv_a (satz154d A)); clear A; intros A.
unfold eq_prat_a in A.
unfold frac_to_prat, nat_to_frac, rep in A.
generalize (redAx1_rev _ _ A); clear A; intros A.
unfold eq_frac_prop in A.
symmetry in A.
rewrite <-satz31 in A.
apply (sqrt_two A).
Qed.

Theorem dense_cut : dense cut lt_cut.
intros x y [a [A B]].
destruct (p4 y a A) as [b [C D]].
exists b. split.
destruct (@satz123H0 x b) as [E|[E|E]].
apply E.
subst x. destruct (B D).
destruct B.
apply satz158b.
apply (satz126 _ b).
apply (satz154a D).
apply E.
exists b.
split. apply C. exact (lt_prat_irreflexive b).
Qed.

Definition pset (X:Prop) := fun a : prat =>
                            if lt_prat a (S O) then True
                                               else if lt_prat a (S (S O)) then X
                                                                           else False.

Lemma pset_p1 (X:Prop) : p1_set (pset X).
intros X. exists O.
exact I.
Qed.

Lemma pset_p2 (X:Prop) : p2_set (pset X).
intros X. exists (S (S O)).
intros [].
Qed.

Lemma pset_p3 (X:Prop) : p3_set (pset X) lt_prat.
intros X a b A B. unfold pset in *.
case_eq (lt_prat b (S O)); intros C.
rewrite (reflect_eq1 (satz86 _ _ _ B (reflect_eq2 C))).
exact I.
rewrite C in A.
case_eq (lt_prat b (S (S O))); intros D.
rewrite D in A.
rewrite (reflect_eq1 (satz86 _ _ _ B (reflect_eq2 D))).
case_eq (lt_prat a (S O)); tauto.
rewrite D in A.
contradiction A.
Qed.

Lemma pset_p4 (X:Prop) : p4_set (pset X) lt_prat.
intros X a A.
unfold pset in *.
case_eq (lt_prat a (S O)); intros B.
destruct (p4 (S O) a (reflect_eq2 B)) as [b [C D]].
exists b. unfold pcut,prat_to_cut,prat_cut_set in C.
rewrite (reflect_eq1 C). tauto.
rewrite B in A.
case_eq (lt_prat a (S (S O))); intros C.
rewrite C in A.
destruct (p4 (S (S O)) a (reflect_eq2 C)) as [b [D E]].
exists b. unfold pcut,prat_to_cut,prat_cut_set in D.
rewrite (reflect_eq1 D).
case_eq (lt_prat b (S O)); tauto.
rewrite C in A.
contradiction A.
Qed.

Definition cp (X:Prop) := Cut (pset X) (pset_p1 X) (pset_p2 X) (pset_p3 X) (pset_p4 X).

Lemma TR_XM : trichotomy cut lt_cut -> XM.
intros tr x.
destruct (tr (cp x) (cp (~x))) as [A|[A|A]].
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.
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.
Qed.

Lemma fe_inv (p q:prat -> Prop) : p = q -> forall a, p a = q a.
intros p q A. rewrite A. tauto.
Qed.

Lemma CE_PE : CE -> PE.
intros cex x y A.
cut (forall a, pcut (cp x) a <-> pcut (cp y) a).
intros B.
generalize (cex (cp x) (cp y) B).
intros C. injection C.
clear C; intros C.
generalize (fe_inv _ _ C).
intros D. exact (D (S O)).
simpl in *.
intros a. unfold pset.
destruct (lt_prat a (S O)). tauto.
destruct (lt_prat a (S (S O))); tauto.
Qed.

Lemma CE_PI : CE -> PI.
exact (fun x => PE_PI (CE_PE x)).
Qed.

Lemma SE_CE : SE -> CE.
intros se [x x1 x2 x3 x4] [y y1 y2 y3 y4] A.
generalize (se _ _ _ A); intros B.
simpl in *. subst x.
generalize (PE_PI (SE_PE se)); intros pi.
rewrite (pi _ x1 y1), (pi _ x2 y2), (pi _ x3 y3), (pi _ x4 y4).
reflexivity.
Qed.

Lemma FE_PE_CE : FE -> PE ->CE.
intros fe pe [x x1 x2 x3 x4] [y y1 y2 y3 y4] A.
generalize (FE_PE_SE fe pe _ _ _ A); intros B.
simpl in *. subst x.
generalize (PE_PI pe); intros pi.
rewrite (pi _ x1 y1), (pi _ x2 y2), (pi _ x3 y3), (pi _ x4 y4).
reflexivity.
Qed.