proposition: Lemma Cauchy_prop3_prop2 : forall seq, Cauchy_prop3 seq -> Cauchy_prop2 seq.
proof: Proof. unfold Cauchy_prop2 in |- *. unfold Cauchy_prop3 in |- *. intros seq H. elim H; intros x H0. exists x. apply Cauchy_Lim_prop3_prop2. assumption. Qed.
imports: CoRN.reals.CReals Coq(Lia)