proposition: Lemma Rseq_cv_neg_pos_infty_mult : Rseq_cv_pos_infty Un -> Rseq_cv_neg_infty Vn -> Rseq_cv_neg_infty (Vn * Un).
proof: Proof. intros Hu Hv M. destruct (Rseq_cv_pos_neg_infty_mult Hu Hv M) as [N HN]. exists N; intros n Hn. unfold Rseq_mult; rewrite Rmult_comm. apply HN; apply Hn. Qed.
imports: Lia Rsequence_def Rsequence_base_facts PeanoNat Rinterval MyRIneq Ranalysis_def Lra