proposition: Fact divides_msum k n f : (forall i, i < n -> divides k (f i)) -> divides k (∑ n f).
proof: Proof. revert f; induction n as [ | n IHn ]; intros f Hf. + rewrite msum_0; apply divides_0. + rewrite msum_S; apply divides_plus. * apply Hf; lia. * apply IHn; intros; apply Hf; lia. Qed.
imports: Arith Lia List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums rel_iter bool_nat power_decomp prime)