proposition: Lemma Eq_alt_2_2 : forall x y : R_Set, (forall e : F, [0] [<] e -> {N : nat | forall m, N <= m -> AbsSmall e (CS_seq F x m[-]CS_seq F y m)}) -> Not (R_ap x y).
proof: Proof. intros x y. case x; intros x_ px. case y; intros y_ py. simpl in |- *. intros H. intro H0. assert (H1 : {e : F | [0] [<] e | {N : nat | forall m : nat, N <= m -> AbsBig (Two[*]e) (x_ m[-]y_ m)}}). elim (R_ap_alt_1 _ _ H0). intros e H1 H2. exists (e [/]TwoNZ). apply pos_div_two; assumption. elim H2; intros N HN. exists N. intros. apply AbsBig_wdl with e; [ auto | rational ]. case H1. intros e H2 H3. case H3; intros N1 A. case (H e H2); intros N2 B. 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. assert (H4 := A NN N1_NN). assert (H5 := B NN N2_NN). unfold AbsSmall in H5. rewrite -> leEq_def in H5. elim H5; intros. elim H4; intros. elim b; intros. rewrite -> leEq_def in H7; apply H7. apply less_leEq_trans with (Two[*]e). astepl ([0][+]e). rstepr (e[+]e). apply plus_resp_less_rht; auto. assumption. apply H6. apply leEq_less_trans with ([--] (Two[*]e)). auto. apply inv_resp_less. astepl ([0][+]e); rstepr (e[+]e). apply plus_resp_less_rht; auto. Qed.
imports: CoRN.algebra.COrdCauchy CoRN.tactics.RingReflection