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