proposition: Lemma str_leEq_seq_so_leEq_Lim : forall (seq : CauchySeq IR) y, (exists N : nat, (forall i, N <= i -> y [<=] seq i)) -> y [<=] Lim seq.
proof: Proof. intros. rewrite -> leEq_def; intro H0. generalize (Lim_less_so_seq_less _ _ H0). elim H; intros N HN. intro H1. elim H1; intros M HM. cut (y [<] y). apply less_irreflexive_unfolded. apply leEq_less_trans with (seq (Nat.max N M)). apply HN; apply Nat.le_max_l. apply HM; apply Nat.le_max_r. Qed.
imports: CoRN.reals.CReals Coq(Lia)