fact: Definition is_limit r l := match l with | minus_inf => Rseq_cv_neg_infty r | finite l => Rseq_cv r l | plus_inf => Rseq_cv_pos_infty r end.
imports: Rbase MyRIneq Rsequence_def Rsequence_facts Rsequence_cv_facts List Option Tactics