proposition: Lemma Cauchy_inv : forall seq : CauchySeqR, Cauchy_prop (fun n => [--] (seq n)).
proof: Proof. intros. apply Cauchy_prop2_prop. unfold Cauchy_prop2 in |- *. exists ([--] (Lim seq)). apply Cauchy_Lim_inv. apply Cauchy_complete. Qed.
imports: CoRN.reals.CReals Coq(Lia)