proposition: Lemma mult_distr_sum0_lft : forall (f : nat -> R) x n, Sum0 n (fun i => x[*]f i) [=] x[*]Sum0 n f.
proof: Proof. intros f x n. induction n as [| n Hrecn]. simpl in |- *; algebra. simpl in |- *. Step_final (x[*]Sum0 n f[+]x[*]f n). Qed.
imports: CoRN.tactics.CornTac CoRN.algebra.CSums CoRN.algebra.CAbMonoids Coq.Sorting.Permutation CoRN.util.SetoidPermutation Coq.Setoids.Setoid Coq.Classes.Morphisms Coq(Lia)