proposition: Lemma Rseq_zip_scal_l : forall An Bn (l : R), l * Rseq_zip An Bn == Rseq_zip (l * An) (l * Bn).
proof: Proof. intros An Bn l n ; unfold Rseq_mult, Rseq_constant, Rseq_zip ; case (n_modulo_2 n) ; intros [p Hp] ; reflexivity. Qed.
imports: MyRIneq Rsequence_def