proposition: Lemma Eq_alt_1 : forall (x y : R_Set) (e : F), [0] [<] e -> Not {N : nat | forall m, N <= m -> AbsBig (e [/]FourNZ) (CS_seq F x m[-]CS_seq F y m)} -> {N : nat | forall m, N <= m -> AbsSmall e (CS_seq F x m[-]CS_seq F y m)}.
proof: Proof. intros x y e H. 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. unfold CS_seq in |- *; intro. case (px e16 He16); intros N1 px2. case (py e16 He16); intros N2 py2. set (NN := Nat.max N1 N2) in *. assert (N1_NN : N1 <= NN). unfold NN in |- *; auto with arith. assert (N2_NN : N2 <= NN). unfold NN in |- *; auto with arith. exists NN. cut (forall m : nat, Not (NN <= m and AbsBig e2 (x_ m[-]y_ m))). intros. unfold AbsSmall in |- *. assert (H3 : Not (AbsBig e2 (x_ m[-]y_ m))). intro; elim (H1 m); split; assumption. assert (H4 : ~ e2 [<=] x_ m[-]y_ m). intro; apply H3; split; try left; assumption. assert (H5 : ~ x_ m[-]y_ m [<=] [--]e2). intro; apply H3; split; try right; assumption. split; rewrite -> leEq_def; intro. apply H5. apply leEq_transitive with ([--]e). apply less_leEq; assumption. apply less_leEq; apply inv_resp_less. unfold e2 in |- *; apply pos_div_two'; assumption. apply H4. apply leEq_transitive with e. apply less_leEq; unfold e2 in |- *; apply pos_div_two'; auto. apply less_leEq; assumption. intro. intro H1. elim H1; intros X Y. elim H0. exists NN. intros. apply AbsBig_wdl with (e2[-]e8[-]e8). 2: unfold e2, e4, e8 in |- *; rational. apply AbsBig_wdr with (x_ m[-]y_ m[-] (x_ m[-]x_ m0) [-] (y_ m0[-]y_ m)). 2: rational. assert (e8 [<] e2). unfold e2, e8 in |- *. rstepl ((e [/]TwoNZ) [/]FourNZ). rstepr (e [/]TwoNZ). apply pos_div_four'. assumption. assert ([0] [<] e2[-]e8). apply plus_cancel_less with e8. rstepl e8. rstepr e2. assumption. assert (e8 [<] e2[-]e8). apply plus_cancel_less with e8. rstepr e2. unfold e2, e8 in |- *; rstepl (e [/]FourNZ). rstepl ((e [/]TwoNZ) [/]TwoNZ). apply pos_div_two'. assumption. apply AbsBigSmall_minus; auto. apply AbsBigSmall_minus; auto. unfold e8 in |- *. rstepl (e [/]SixteenNZ[+]e [/]SixteenNZ). rstepr (x_ m[-]x_ N1[+] (x_ N1[-]x_ m0)). apply AbsSmall_plus. apply px2. apply Nat.le_trans with NN; assumption. apply AbsSmall_minus. apply px2. apply Nat.le_trans with NN; assumption. unfold e8 in |- *. rstepl (e [/]SixteenNZ[+]e [/]SixteenNZ). rstepr (y_ m0[-]y_ N2[+] (y_ N2[-]y_ m)). apply AbsSmall_plus. apply py2. apply Nat.le_trans with NN; assumption. apply AbsSmall_minus. apply py2. apply Nat.le_trans with NN; assumption. Qed.
imports: CoRN.algebra.COrdCauchy CoRN.tactics.RingReflection