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