proposition: Lemma Rseq_cv_neg_infty_opp_compat : Rseq_cv_neg_infty Un -> Rseq_cv_pos_infty (- Un).
proof: Proof. intros H M. destruct (H (- M)%R) as [N HN]. exists N; intros n Hn. unfold Rseq_opp. pattern M; rewrite <- Ropp_involutive. apply Ropp_lt_gt_contravar. apply HN; assumption. Qed.
imports: Lia Rsequence_def Rsequence_base_facts PeanoNat Rinterval MyRIneq Ranalysis_def Lra