proposition: Lemma Rseq_equiv_1 : forall Un Vn, (forall n, Vn n <> 0) -> (Rseq_div Un Vn) ~ 1 -> Un ~ Vn.
proof: Proof. intros Un Vn Hneq H. apply Rseq_equiv_sym in H. apply Rseq_equiv_sym. intros eps Heps. destruct (H eps Heps) as [N HN]. exists N. intros n Hn. unfold Rseq_minus, Rseq_div, Rseq_constant in *. replace (eps * Rabs (IZR 1))%R with eps in HN by (rewrite Rabs_R1; ring). replace (Vn n - Un n)%R with ((1 - Un n / Vn n)* (Vn n))%R by (field; trivial). rewrite Rabs_mult. apply Rmult_le_compat_r. apply Rabs_pos. apply HN; assumption. Qed.
imports: PeanoNat Reals Setoid Morphisms Rsequence_def Rsequence_base_facts Rsequence_cv_facts Lra