proposition: Lemma aew_Cauchy2 : forall c, Cauchy_Lim_prop2 x c -> Cauchy_Lim_prop2 y c.
proof: Proof. intros c H. red in |- *; intros eps H0. elim (H eps H0). intros N HN. elim aew_equal; intros n Hn. exists (Nat.max n N). intros. apply AbsSmall_wdr_unfolded with (x m[-]c). apply HN; apply Nat.le_trans with (Nat.max n N); auto with arith. apply cg_minus_wd; [ apply Hn | algebra ]. apply Nat.le_trans with (Nat.max n N); auto with arith. Qed.
imports: CoRN.reals.CSumsReals CoRN.reals.NRootIR Coq(Lia)