proposition: Lemma Rseq_equiv_sym : forall Un Vn, Un ~ Vn -> Vn ~ Un.
proof: Proof. intros Un Vn H eps Heps. pose (eps' := (eps / (1 + eps))%R). assert (Heps' : eps' > 0). apply Rmult_gt_0_compat; [assumption|apply Rinv_0_lt_compat; lra]. destruct (H eps') as [N HN]; [assumption|]. exists N; intros n Hn. unfold Rseq_minus; rewrite Rabs_minus_sym. apply Rmult_le_reg_l with (/(1 + eps))%R; [apply Rinv_0_lt_compat; lra|]. rewrite <- Rmult_assoc. replace (/(1 + eps))%R with (1 - eps')%R by (unfold eps'; field; apply Rgt_not_eq; lra). replace ((1 - eps') * eps)%R with eps' by (unfold eps'; field; apply Rgt_not_eq; lra). rewrite <- Rplus_0_r. rewrite <- Rplus_opp_r with (eps' * Rabs (Un n - Vn n))%R. unfold Rminus; rewrite Rmult_plus_distr_r. rewrite Rmult_1_l. rewrite <- Rplus_assoc. rewrite <- Ropp_mult_distr_l_reverse. apply Rplus_le_compat_r. eapply Rle_trans. apply HN; assumption. rewrite <- Rmult_plus_distr_l. apply Rmult_le_compat_l; [left; assumption|]. replace (Rabs (Vn n) + Rabs (Un n + - Vn n))%R with (Rabs (Un n + - Vn n) + Rabs (Vn n))%R by field. pattern Un at 2; replace (Un n) with (Un n - Vn n + Vn n)%R by field. apply Rabs_triang. Qed.
imports: PeanoNat Reals Setoid Morphisms Rsequence_def Rsequence_base_facts Rsequence_cv_facts Lra