proposition: Lemma Lim_ap_imp_seq_ap' : forall seq1 seq2 : CauchySeq IR, Lim seq1 [#] Lim seq2 -> {N : nat | seq1 N [#] seq2 N}.
proof: Proof. intros seq1 seq2 H. elim (Lim_ap_imp_seq_ap _ _ H); intros N HN. exists N; apply HN. apply le_n. Qed.
imports: CoRN.reals.CReals Coq(Lia)