proposition: Lemma R_ap_alt_2 : forall x y : R_CSetoid, {e : F | [0] [<] e | {N : nat | forall m, N <= m -> AbsBig e (CS_seq F x m[-]CS_seq F y m)}} -> x [#] y.
proof: Proof. intros x y H. case H. intros e H0. set (e2 := e [/]TwoNZ) in *. set (e4 := e [/]FourNZ) in *. set (e8 := e [/]EightNZ) in *. set (e16 := e [/]SixteenNZ) in *. assert (He2 : [0] [<] e2). unfold e2 in |- *; apply pos_div_two; assumption. assert (He4 : [0] [<] e4). unfold e4 in |- *; apply pos_div_four; assumption. assert (He8 : [0] [<] e8). unfold e8 in |- *; apply pos_div_eight; assumption. assert (He16 : [0] [<] e16). unfold e16 in |- *; apply pos_div_sixteen; assumption. case x; intros x_ px. case y; intros y_ py. case (px e16 He16); intros N1 H31. case (py e16 He16); intros N2 H41. simpl in |- *; intro H2; case H2; intros N H21. set (NN := Nat.max N (Nat.max N1 N2)) in *. assert (N_NN : N <= NN). unfold NN in |- *; auto with arith. assert (N1_NN : N1 <= NN). unfold NN in |- *; apply Nat.le_trans with (Nat.max N1 N2); auto with arith. assert (N2_NN : N2 <= NN). unfold NN in |- *; apply Nat.le_trans with (Nat.max N1 N2); auto with arith. set (x0 := x_ NN) in *. set (y0 := y_ NN) in *. simpl in |- *. unfold R_ap in |- *. unfold R_lt in |- *. simpl in |- *. assert (H5 : AbsBig e2 (x0[-]y0)). assert (e2 [<=] e). unfold e2 in |- *; apply less_leEq; apply pos_div_two'; auto. split; auto. elim (H21 NN). intros H' Haux; elim Haux; intros; [ left | right ]. apply leEq_transitive with e; auto. apply leEq_transitive with ([--]e); auto; apply inv_resp_leEq; auto. unfold NN in |- *; auto with arith. case H5; intros Hx s; case s; intro H6. right. exists NN. exists e4. assumption. intro m; intros. astepl ([--]e8[+]e2[+][--]e8). 2: unfold e2, e8, e4 in |- *; rational. rstepr (x_ m[-]x0[+] (x0[-]y0) [+] (y0[-]y_ m)). apply plus_resp_leEq_both. apply plus_resp_leEq_both. astepl ([--]e16[+][--]e16). 2: unfold e16, e8 in |- *; rational. rstepr (x_ m[-]x_ N1[+] (x_ N1[-]x0)). apply plus_resp_leEq_both. assert (H7 : AbsSmall e16 (x_ m[-]x_ N1)). apply H31; apply Nat.le_trans with NN; auto. elim H7; intros. rstepl ([--]e16). assumption. assert (H7 : AbsSmall e16 (x_ N1[-]x0)). apply AbsSmall_minus. unfold x0 in |- *; auto. elim H7; intros. rstepl ([--]e16). assumption. assumption. astepl ([--]e16[+][--]e16). 2: unfold e16, e8 in |- *; rational. rstepr (y0[-]y_ N2[+] (y_ N2[-]y_ m)). apply plus_resp_leEq_both. assert (H7 : AbsSmall e16 (y0[-]y_ N2)). unfold y0 in |- *; auto. elim H7; intros. rstepl ([--]e16). assumption. assert (H7 : AbsSmall e16 (y_ N2[-]y_ m)). apply AbsSmall_minus. apply H41. apply Nat.le_trans with NN; auto. elim H7; intros. rstepl ([--]e16). assumption. left. exists NN. exists e4. assumption. intro m; intros. astepl ([--]e8[+]e2[+][--]e8). 2: unfold e8, e2, e4 in |- *; rational. rstepr (y_ m[-]y0[+] (y0[-]x0) [+] (x0[-]x_ m)). apply plus_resp_leEq_both. apply plus_resp_leEq_both. astepl ([--]e16[+][--]e16). 2: unfold e16, e8 in |- *; rational. rstepr (y_ m[-]y_ N2[+] (y_ N2[-]y0)). apply plus_resp_leEq_both. assert (H8 : AbsSmall e16 (y_ m[-]y_ N2)). apply H41. apply Nat.le_trans with NN; auto. elim H8; intros. rstepl ([--]e16). assumption. assert (H8 : AbsSmall e16 (y_ N2[-]y0)). apply AbsSmall_minus. unfold y0 in |- *; auto. elim H8; intros. rstepl ([--]e16). assumption. apply inv_cancel_leEq. rstepl (x0[-]y0). assumption. astepl ([--]e16[+][--]e16). 2: unfold e16, e8 in |- *; rational. rstepr (x0[-]x_ N1[+] (x_ N1[-]x_ m)). apply plus_resp_leEq_both. assert (H8 : AbsSmall e16 (x0[-]x_ N1)). unfold x0 in |- *; auto. elim H8; intros. rstepl ([--]e16). assumption. assert (H8 : AbsSmall e16 (x_ N1[-]x_ m)). apply AbsSmall_minus. apply H31. apply Nat.le_trans with NN; auto. elim H8; intros. rstepl ([--]e16). assumption. Qed.
imports: CoRN.algebra.COrdCauchy CoRN.tactics.RingReflection