proposition: Lemma convergent_wd : (forall n, x n [=] y n) -> convergent x -> convergent y.
proof: Proof. intros H H0. red in |- *; red in H0. apply Cauchy_prop_wd with (seq_part_sum x). assumption. intro. unfold seq_part_sum in |- *. apply Sum0_wd. assumption. Qed.
imports: CoRN.reals.CSumsReals CoRN.reals.NRootIR Coq(Lia)