proposition: Fact square_sum n f : (∑ n f)*(∑ n f) = ∑ n (fun i => f i*f i) + 2*∑ n (fun i => ∑ i (fun j => f i*f j)).
proof: Proof. rewrite product_sums, <- sum_0n_scal_l; f_equal. apply msum_ext; intros; rewrite <- sum_0n_scal_l. apply msum_ext; intros; ring. Qed.
imports: Arith Lia List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums rel_iter bool_nat power_decomp prime)