proposition: Fact product_sums n f g : (∑ n f)*(∑ n g) = ∑ n (fun i => f i*g i) + ∑ n (fun i => ∑ i (fun j => f i*g j + f j*g i)).
proof: Proof. induction n as [ | n IHn ]. + repeat rewrite msum_0; auto. + repeat rewrite msum_plus1; auto. repeat rewrite Nat.mul_add_distr_l. repeat rewrite Nat.mul_add_distr_r. rewrite IHn, msum_sum; auto. * rewrite sum_0n_scal_l, sum_0n_scal_r; ring. * intros; ring. Qed.
imports: Arith Lia List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums rel_iter bool_nat power_decomp prime)