proposition: Lemma Rseq_equiv_inv_compat : forall Un Vn, {m | forall n, (n >= m)%nat -> Un n <> 0} -> {m | forall n, (n >= m)%nat -> Vn n <> 0} -> Un ~ Vn -> (Rseq_inv Un) ~ (Rseq_inv Vn).
proof: Proof. intros Un Vn Upos Vpos H eps Heps. apply Rseq_equiv_sym in H. destruct (H eps Heps) as [N HN]. destruct Upos as (m1, Upos). destruct Vpos as (m2, Vpos). exists (Nat.max (Nat.max N m1) m2); intros n Hn. unfold Rseq_minus, Rseq_inv in *. assert (Hm1 : (n >= m1)%nat). apply Nat.le_trans with (Nat.max (Nat.max N m1) m2). apply Nat.le_trans with (Nat.max N m1). intuition (auto with arith). intuition (auto with arith). intuition. assert (Hm2 : (n >= m2)%nat). apply Nat.le_trans with (Nat.max (Nat.max N m1) m2). intuition (auto with arith). intuition. assert (HN1 : (n >= N)%nat). apply Nat.le_trans with (Nat.max (Nat.max N m1) m2). apply Nat.le_trans with (Nat.max N m1). intuition (auto with arith). intuition (auto with arith). intuition. replace (/ Un n - / Vn n)%R with ((Vn n - Un n) */ (Un n * Vn n))%R by (field; auto). rewrite Rabs_mult. replace (Rabs (/Un n))%R with (Rabs (Vn n) * (Rabs (/ (Un n * Vn n))))%R. rewrite <- Rmult_assoc. apply Rmult_le_compat_r. apply Rabs_pos. auto. rewrite <- Rabs_mult. replace (Vn n * / (Un n * Vn n))%R with (/ Un n)%R by (field; auto); reflexivity. Qed.
imports: PeanoNat Reals Setoid Morphisms Rsequence_def Rsequence_base_facts Rsequence_cv_facts Lra