proposition: Lemma Rseq_sum_constant_compat: forall (l : R) n, (Rseq_sum l n = INR (S n) * l)%R.
proof: Proof. intros l n ; induction n. simpl ; symmetry ; apply Rmult_1_l. rewrite Rseq_sum_simpl, S_INR, IHn ; unfold Rseq_constant ; ring. Qed.
imports: Lia Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rewrite_facts Rpser_def Rpser_def_simpl MyRIneq MyNat Lra