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