proposition: Lemma Rseq_positive_limit : forall (An : nat -> R) (a : R), (forall n, 0 <= An n) -> Rseq_cv An a -> 0 <= a.
proof: Proof. intros An a Hpos Ha. apply Rnot_lt_le; intro Na. destruct (Ha (Ropp (Rdiv a 2))) as [N HN]; [lra | ]. pose proof (HN N (le_n N)). generalize dependent H. unfold R_dist, Rabs. pose proof Hpos N as Hposn. destruct (Rcase_abs (An N - a)); intro; lra. Qed.
imports: Lia Rsequence_def Rsequence_base_facts PeanoNat Rinterval MyRIneq Ranalysis_def Lra