proposition: Lemma mult_distr_sum_lft : forall (f : nat -> R) x m n, Sum m n (fun i => x[*]f i) [=] x[*]Sum m n f.
proof: Proof. intros f x m n. unfold Sum in |- *. unfold Sum1 in |- *. Step_final (x[*]Sum0 (S n) f[-]x[*]Sum0 m f). 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)