proposition: Lemma R_lt_cotrans : cotransitive R_lt.
proof: Proof. red in |- *. intros x y. elim x; intros x_ px. elim y; intros y_ py. intros Hxy z. elim z; intros z_ pz. elim Hxy; intros N H. elim H; clear Hxy H; intros e He HN. simpl in HN. set (e3 := e [/]ThreeNZ) in *. cut ([0] [<] e3); [ intro He3 | unfold e3 in |- *; apply pos_div_three; auto ]. set (e6 := e [/]SixNZ) in *. cut ([0] [<] e6); [ intro He6 | unfold e6 in |- *; apply pos_div_six; auto ]. set (e12 := e [/]TwelveNZ) in *. cut ([0] [<] e12); [ intro He12 | unfold e12 in |- *; apply pos_div_twelve; auto ]. set (e24 := e [/]TwentyFourNZ) in *. cut ([0] [<] e24); [ intro He24 | unfold e24 in |- *; apply pos_div_twentyfour; auto ]. elim (px e24 He24); intros Nx HNx. elim (py e24 He24); intros Ny HNy. elim (pz e24 He24); intros Nz HNz. set (NN := Nat.max N (Nat.max Nx (Nat.max Ny Nz))) in *. set (x0 := x_ NN) in *. set (y0 := y_ NN) in *. set (z0 := z_ NN) in *. elim (less_cotransitive_unfolded _ (x0[+]e3) (y0[-]e3)) with z0. intro Hyz. left. exists NN; exists e6; auto. intros n Hn; simpl in |- *. apply leEq_wdl with (e3[-] (e24[+]e24[+]e24[+]e24)). 2: unfold e3, e6, e12, e24 in |- *; rational. apply leEq_transitive with (e3[-] (z0[-]z_ Nz[+] (z_ Nz[-]z_ n) [+] (x_ n[-]x_ Nx) [+] (x_ Nx[-]x0))). apply minus_resp_leEq_rht. repeat apply plus_resp_leEq_both. unfold z0 in |- *; elim (HNz NN); auto; unfold NN in |- *; eauto with arith. apply shift_minus_leEq; apply shift_leEq_plus'. unfold cg_minus in |- *; apply shift_plus_leEq'. elim (HNz n); auto; apply Nat.le_trans with NN; auto; unfold NN in |- *; eauto with arith. elim (HNx n); auto; apply Nat.le_trans with NN; auto; unfold NN in |- *; eauto with arith. apply shift_minus_leEq; apply shift_leEq_plus'. unfold cg_minus in |- *; apply shift_plus_leEq'. unfold x0 in |- *; elim (HNx NN); auto; unfold NN in |- *; eauto with arith. apply shift_minus_leEq. rstepr (z0[-]x0). apply shift_leEq_minus; astepl (x0[+]e3); apply less_leEq; auto. intro Hzx. right. exists NN; exists e6; auto. intros n Hn; simpl in |- *. apply leEq_wdl with (e3[-] (e24[+]e24[+]e24[+]e24)). 2: unfold e3, e6, e12, e24 in |- *; rational. apply leEq_transitive with (e3[-] (z_ Nz[-]z0[+] (z_ n[-]z_ Nz) [+] (y_ Ny[-]y_ n) [+] (y0[-]y_ Ny))). apply minus_resp_leEq_rht. repeat apply plus_resp_leEq_both. apply shift_minus_leEq; apply shift_leEq_plus'. unfold cg_minus in |- *; apply shift_plus_leEq'. unfold z0 in |- *; elim (HNz NN); auto; unfold NN in |- *; eauto with arith. elim (HNz n); auto; apply Nat.le_trans with NN; auto; unfold NN in |- *; eauto with arith. apply shift_minus_leEq; apply shift_leEq_plus'. unfold cg_minus in |- *; apply shift_plus_leEq'. elim (HNy n); auto; apply Nat.le_trans with NN; auto; unfold NN in |- *; eauto with arith. unfold y0 in |- *; elim (HNy NN); auto; unfold NN in |- *; eauto with arith. apply shift_minus_leEq. rstepr (y0[-]z0). apply shift_leEq_minus; apply shift_plus_leEq'; apply less_leEq; auto. apply shift_less_minus. astepl (x0[+] (e3[+]e3)); apply shift_plus_less'. apply less_leEq_trans with e. apply shift_plus_less. apply less_wdl with ((e[-]e3) [/]TwoNZ). 2: unfold e3 in |- *; rational. apply pos_div_two'. apply shift_less_minus; astepl e3; unfold e3 in |- *; apply pos_div_three'; auto. unfold x0, y0, NN in |- *; apply HN; eauto with arith. Qed.
imports: CoRN.algebra.COrdCauchy CoRN.tactics.RingReflection