proposition: Lemma Rseq_cv_pos_neg_infty_mult : Rseq_cv_pos_infty Un -> Rseq_cv_neg_infty Vn -> Rseq_cv_neg_infty (Un * Vn).
proof: Proof. intros Hu Hv M. destruct (Hu (Rabs M)%R) as [Nu HNu]. destruct (Hv (-1)) as [Nv HNv]. exists (Nat.max Nu Nv); intros n Hn. unfold Rseq_mult. apply Rlt_le_trans with (- Rabs M)%R. replace (Un n * Vn n)%R with (-(Un n * (- Vn n)))%R by ring. apply Ropp_lt_contravar. replace (Rabs M)%R with ((Rabs M) * (- - 1))%R by ring. apply Rmult_le_0_lt_compat. apply Rabs_pos. lra. apply HNu; eapply Nat.le_trans; [apply Nat.le_max_l|eexact Hn]. apply Ropp_lt_contravar; apply HNv; eapply Nat.le_trans; [apply Nat.le_max_r|eexact Hn]. replace M with (- -M)%R by ring; apply Ropp_le_contravar; rewrite Ropp_involutive. rewrite <- Rabs_Ropp. apply RRle_abs. Qed.
imports: Lia Rsequence_def Rsequence_base_facts PeanoNat Rinterval MyRIneq Ranalysis_def Lra