proposition: Lemma Rseq_little_O_inv_contravar : Un = o(Vn) -> Rseq_neq_0 Un -> Rseq_neq_0 Vn -> (/ Vn) = o(/ Un).
proof: Proof. intros Hu Hnu Hnv. intros eps Heps. destruct (Hu eps) as [N HN]; [assumption|]. exists N; intros n Hn. unfold Rseq_inv. rewrite Rabs_inv. rewrite Rabs_inv. apply (Rmult_le_reg_l (Rabs (Un n))); [apply Rabs_pos_lt; apply Hnu|]. apply (Rmult_le_reg_l (Rabs (Vn n))); [apply Rabs_pos_lt; apply Hnv|]. field_simplify. try (unfold Rdiv; rewrite Rinv_1; repeat rewrite Rmult_1_r). rewrite Rmult_comm; apply HN; apply Hn. apply Rabs_no_R0; apply Hnu. apply Rabs_no_R0; apply Hnv. Qed.
imports: PeanoNat Reals Setoid Morphisms Rsequence_def Rsequence_base_facts Rsequence_cv_facts Lra