proposition: Lemma aew_Cauchy : Cauchy_prop x -> Cauchy_prop y.
proof: Proof. intro H. red in |- *; intros e H0. elim (H _ (pos_div_two _ _ H0)). intros N HN. elim aew_equal; intros n Hn. exists (Nat.max n N). intros. apply AbsSmall_wdr_unfolded with (x m[-]x (Nat.max n N)). rstepr (x m[-]x N[+] (x N[-]x (Nat.max n N))). rstepl (e [/]TwoNZ[+]e [/]TwoNZ). apply AbsSmall_plus. apply HN; apply Nat.le_trans with (Nat.max n N); auto with arith. apply AbsSmall_minus; apply HN; apply Nat.le_trans with (Nat.max n N); auto with arith. apply cg_minus_wd; apply Hn. apply Nat.le_trans with (Nat.max n N); auto with arith. apply Nat.le_max_l. Qed.
imports: CoRN.reals.CSumsReals CoRN.reals.NRootIR Coq(Lia)