proposition: Fact sum_0n_distr_in_out n a b f : ∑ n (fun i => (a i+b i) * f i) = ∑ n (fun i => a i * f i) + ∑ n (fun i => b i * f i).
proof: Proof. rewrite <- msum_sum; auto. + apply msum_ext; intros; ring. + intros; ring. Qed.
imports: Arith Nat Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd rel_iter sums)