proposition: Lemma Rseq_sum_ext_strong : forall Un Vn n, (forall p, (p <= n)%nat -> Un p = Vn p) -> Rseq_sum Un n = Rseq_sum Vn n.
proof: Proof. intros Un Vn n ; induction n ; intro Heq. simpl ; apply Heq ; trivial. do 2 rewrite Rseq_sum_simpl ; rewrite IHn, Heq. reflexivity. trivial. intros ; apply Heq ; auto. Qed.
imports: Lia Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rewrite_facts Rpser_def Rpser_def_simpl MyRIneq MyNat Lra