proposition: Lemma Cprop2_seq_imp_Cprop2_subseq : forall a, Cauchy_Lim_prop2 seq2 a -> Cauchy_Lim_prop2 seq1 a.
proof: Proof. intros a H. red in |- *; red in H. intros eps H0. elim (H _ H0). intros N HN. elim (unbnd_f N); intros i Hi. exists i. intros. astepr (seq2 (f m) [-]a). apply HN. cut (f i <= f m). intros; apply Nat.le_trans with (f i); auto with arith. apply monF; assumption. Qed.
imports: CoRN.reals.Max_AbsIR CoRN.algebra.Expon CoRN.algebra.CPoly_ApZero