fact: Definition rseq_limit_opp l := match l with | minus_inf => plus_inf | finite u => finite (- u) | plus_inf => minus_inf end.
imports: Rbase MyRIneq Rsequence_def Rsequence_facts Rsequence_cv_facts List Option Tactics