proposition: Lemma Rseq_cv_pos_pos_infty_mult : Rseq_cv_pos_infty Un -> Rseq_cv_pos_infty Vn -> Rseq_cv_pos_infty (Un * Vn).
proof: Proof. intros Hu Hv M. destruct (Hu (Rabs M)) 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 (Rabs M) with ((Rabs M)*1)%R by apply Rmult_1_r. apply Rmult_le_0_lt_compat. apply Rabs_pos. apply Rle_0_1. apply HNu; eapply Nat.le_trans; [apply Nat.le_max_l|eexact Hn]. 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