proposition: Lemma Rseq_cv_neg_neg_infty_mult : Rseq_cv_neg_infty Un -> Rseq_cv_neg_infty Vn -> Rseq_cv_pos_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 Rle_lt_trans with (Rabs M). apply RRle_abs. replace (Un n * Vn n)%R with ((- Un n) *( - Vn n))%R by ring. replace (Rabs M)%R with (( - -Rabs M) *( - - 1))%R by ring. apply Rmult_le_0_lt_compat. rewrite Ropp_involutive; apply Rabs_pos. lra. apply Ropp_lt_contravar; 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]. Qed.
imports: Lia Rsequence_def Rsequence_base_facts PeanoNat Rinterval MyRIneq Ranalysis_def Lra