proposition: Lemma Lim_ap_imp_seq_ap : forall seq1 seq2 : CauchySeq IR, Lim seq1 [#] Lim seq2 -> {N : nat | forall m, N <= m -> seq1 m [#] seq2 m}.
proof: Proof. intros seq1 seq2 H. elim (ap_imp_less _ _ _ H); intro. elim (Lim_less_Lim_so_seq_less_seq _ _ a); intros N HN. exists N; intros. apply less_imp_ap; apply HN; assumption. elim (Lim_less_Lim_so_seq_less_seq _ _ b); intros N HN. exists N; intros. apply Greater_imp_ap; apply HN; assumption. Qed.
imports: CoRN.reals.CReals Coq(Lia)