proposition: Lemma Rseq_cv_eq_compat1 : forall Un Vn l, {m | forall n, (n >= m)%nat -> Un n = Vn n} -> Rseq_cv Un l -> Rseq_cv Vn l.
proof: Proof. intros Un Vn l Heq Hseq. intros eps Heps. destruct Heq as (m, Heq). destruct (Hseq eps Heps) as (N, Hseq2). exists (max N m). intros n Hn. assert (Hm : (n >= m)%nat). apply Nat.le_trans with (max N m) ; intuition. unfold R_dist in *. rewrite <- (Heq n) ; intuition; try (apply Hseq2; intuition; apply Nat.le_trans with (max N m) ; intuition). Qed.
imports: PeanoNat Reals Rintegral Rintegral_usual Rintegral_tactic Lia Lra Rsequence_facts Rsequence_subsequence Rpser RTaylor MyRfunctions Rsequence_tactics