proposition: Lemma Rseq_equiv_cv_div : (forall n, Vn n <> 0) -> Rseq_cv (Un / Vn) 1.
proof: Proof. intros Hv eps Heps. apply Rseq_equiv_sym in Heq. destruct (Heq (eps / 2))%R as [N HN]; [lra|]. exists N; intros n Hn. unfold R_dist, Rseq_div. replace (Un n / Vn n - 1)%R with ((Un n - Vn n) / Vn n)%R by (field; apply Hv). unfold Rdiv. rewrite Rabs_mult; rewrite Rabs_inv. rewrite Rabs_minus_sym. rewrite Rmult_comm. apply (Rmult_lt_reg_l (Rabs (Vn n))). apply Rabs_pos_lt; apply Hv. rewrite <- Rmult_assoc. rewrite Rinv_r; [|apply Rabs_no_R0; apply Hv]. rewrite Rmult_1_l. eapply Rle_lt_trans. apply HN; exact Hn. rewrite Rmult_comm. apply Rmult_lt_compat_l. apply Rabs_pos_lt; apply Hv. lra. Qed.
imports: PeanoNat Reals Setoid Morphisms Rsequence_def Rsequence_base_facts Rsequence_cv_facts Lra