proposition: Lemma Lim_strext : forall seq1 seq2 : CauchySeq IR, Lim seq1 [#] Lim seq2 -> {n : nat | seq1 n [#] seq2 n}.
proof: Proof. intros seq1 seq2 H. cut ({n : nat | seq1 n [<] seq2 n} or {n : nat | seq2 n [<] seq1 n}). intro H0; inversion_clear H0; rename X into H1; elim H1; intros n Hn. exists n; apply less_imp_ap; assumption. exists n; apply Greater_imp_ap; assumption. cut (Lim seq1 [<] Lim seq2 or Lim seq2 [<] Lim seq1). intros H0. 2: apply ap_imp_less; assumption. inversion_clear H0; [ left | right ]. cut {n : nat | forall m : nat, n <= m -> seq1 m [<] seq2 m}. 2: apply Lim_less_Lim_so_seq_less_seq; assumption. intro H0; elim H0; intros N HN. exists N; apply HN; auto with arith. cut {n : nat | forall m : nat, n <= m -> seq2 m [<] seq1 m}. 2: apply Lim_less_Lim_so_seq_less_seq; assumption. intro H0; elim H0; intros N HN. exists N; apply HN; auto with arith. Qed.
imports: CoRN.reals.CReals Coq(Lia)