proposition: Lemma Rseq_cv_div_compat : forall Un Vn lu lv, Rseq_cv Un lu -> Rseq_cv Vn lv -> lv <> 0 -> Rseq_cv (Un / Vn) (lu / lv).
proof: Proof. intros Un Vn lu lv Hu Hv H. unfold Rseq_div, Rdiv. apply Rseq_cv_eq_compat with (Un * (/ Vn)). intros n; reflexivity. apply Rseq_cv_mult_compat; [apply Hu|]. apply Rseq_cv_inv_compat; [apply Hv|apply H]. Qed.
imports: Lia Rsequence_def Rsequence_base_facts PeanoNat Rinterval MyRIneq Ranalysis_def Lra