proposition: Lemma Rseq_negative_limit : forall (An : nat -> R) (a : R), (forall n, An n <= 0) -> Rseq_cv An a -> a <= 0.
proof: Proof. intros An a Hneg Ha ; apply Ropp_le_cancel ; rewrite Ropp_0 ; eapply Rseq_positive_limit, Rseq_cv_opp_compat, Ha. intro n ; apply Ropp_0_ge_le_contravar, Rle_ge, Hneg. Qed.
imports: Lia Rsequence_def Rsequence_base_facts PeanoNat Rinterval MyRIneq Ranalysis_def Lra