proposition: Lemma Rseq_sum_scal_compat_r : forall (l : R) Un, Rseq_sum (Un * l) == Rseq_sum Un * l.
proof: Proof. intros l Un n ; induction n. reflexivity. simpl ; rewrite IHn ; unfold Rseq_mult, Rseq_constant ; simpl ; ring. Qed.
imports: Lia Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rewrite_facts Rpser_def Rpser_def_simpl MyRIneq MyNat Lra