proposition: Lemma is_limit_ext : forall r s k l, is_limit r k -> r == s -> k = l -> is_limit s l.
proof: Proof. intros r s k [] Hrk Hrs Hkl ; [ eapply Rseq_cv_neg_infty_eq_compat | eapply Rseq_cv_eq_compat ; [symmetry |] | eapply Rseq_cv_pos_infty_eq_compat ] ; subst ; eassumption. Qed.
imports: Rbase MyRIneq Rsequence_def Rsequence_facts Rsequence_cv_facts List Option Tactics