proposition: Lemma Rseq_cv_Rseq_cv_neg_infty_incompat : forall An l, Rseq_cv An l -> Rseq_cv_neg_infty An -> False.
proof: Proof. intros ; eapply Rseq_cv_Rseq_cv_pos_infty_incompat. eapply Rseq_cv_opp_compat ; eassumption. eapply Rseq_cv_neg_infty_opp_compat ; eassumption. Qed.
imports: Lia Rsequence_def Rsequence_base_facts PeanoNat Rinterval MyRIneq Ranalysis_def Lra