fact: Definition rseq_limit_add ll lr := match ll, lr with | minus_inf, plus_inf => None | plus_inf , minus_inf => None | minus_inf, _ => Some minus_inf | _ , minus_inf => Some minus_inf | plus_inf , _ => Some plus_inf | _ , plus_inf => Some plus_inf | finite u , finite v => Some (finite (u + v)) end.
imports: Rbase MyRIneq Rsequence_def Rsequence_facts Rsequence_cv_facts List Option Tactics