proposition: Lemma Rseq_cv_neg_infty_div_compat : forall l, Rseq_cv_neg_infty Un -> Rseq_cv Vn l -> Rseq_cv (Vn / Un) 0.
proof: Proof. intros l HU HV. assert (H : Rseq_cv (Vn*(/Un)) 0). rewrite <- Rmult_0_r with l. apply Rseq_cv_mult_compat. apply HV. apply Rseq_cv_neg_infty_inv_compat; apply HU. unfold Rseq_mult in H. unfold Rseq_div, Rdiv. apply H. Qed.
imports: Lia Rsequence_def Rsequence_base_facts PeanoNat Rinterval MyRIneq Ranalysis_def Lra