proposition: Theorem Newton_nat a b n : power n (a + b) = ∑ (S n) (fun i => binomial n i * power (n - i) a * power i b).
proof: Proof. rewrite binomial_Newton with (1 := Nat_plus_monoid) (4 := Nat_mult_monoid); try (intros; ring); auto. apply msum_ext; intros i Hi. rewrite scal_one with (1 := Nat_plus_monoid) (3 := Nat_mult_monoid); auto; try (intros; ring). rewrite <-Nat.mul_assoc; f_equal; auto. generalize (binomial n i); intros k. induction k as [ | k IHk ]. + rewrite mscal_0; auto. + rewrite mscal_S, IHk; auto; apply plus_cancel_l. Qed.
imports: List Arith ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list binomial)