proposition: Lemma Rseq_equiv_trans : forall Un Vn Wn, Un ~ Vn -> Vn ~ Wn -> Un ~ Wn.
proof: Proof. intros Un Vn Wn Hu Hv eps Heps. pose (eps' := Rmin 1 (eps / 3)). assert (Heps' : 0 < eps'). compute; destruct Rle_dec; lra. assert (Heps2 : eps' * eps' <= eps'). pattern eps' at 3; replace eps' with (1 * eps')%R by field. apply Rmult_le_compat; (auto with real || apply Rmin_l). destruct (Hu eps') as [Nu HNu]; [assumption|]. destruct (Hv eps') as [Nv HNv]; [assumption|]. exists (Nat.max Nu Nv); intros n Hn. replace eps with (eps / 3 + (eps / 3 + eps / 3))%R by field. do 2 rewrite Rmult_plus_distr_r. unfold Rseq_minus. eapply Rle_trans; [apply R_dist_tri with (z := Vn n)|]. apply Rplus_le_compat. eapply Rle_trans. apply HNu; eapply Nat.le_trans; [apply Nat.le_max_l|eexact Hn]. apply Rmult_le_compat_r; [apply Rabs_pos|apply Rmin_r]. eapply Rle_trans. apply HNv; eapply Nat.le_trans; [apply Nat.le_max_r|eexact Hn]. replace (Vn n) with ((Vn n - Un n) + Un n)%R by field. eapply Rle_trans. apply Rmult_le_compat_l; [lra|apply Rabs_triang]. rewrite Rmult_plus_distr_l. apply Rplus_le_compat. eapply Rle_trans. apply Rmult_le_compat_l; [left; assumption|]. rewrite Rabs_minus_sym. apply HNu; eapply Nat.le_trans; [apply Nat.le_max_l|eexact Hn]. rewrite <- Rmult_assoc; apply Rmult_le_compat_r; [apply Rabs_pos|]. eapply Rle_trans; [eexact Heps2|apply Rmin_r]. apply Rmult_le_compat_r; [apply Rabs_pos|apply Rmin_r]. Qed.
imports: PeanoNat Reals Setoid Morphisms Rsequence_def Rsequence_base_facts Rsequence_cv_facts Lra