proposition: Lemma Eq_alt_2_1 : forall x y : R_Set, Not (R_ap x y) -> forall e : F, [0] [<] e -> {N : nat | forall m, N <= m -> AbsSmall e (CS_seq F x m[-]CS_seq F y m)}.
proof: Proof. intros. apply Eq_alt_1. assumption. intro. apply H. apply R_ap_alt_2. exists (e [/]FourNZ). apply pos_div_four; auto. assumption. Qed.
imports: CoRN.algebra.COrdCauchy CoRN.tactics.RingReflection