proposition: Theorem Newton_nat_S a n : power n (1 + a) = ∑ (S n) (fun i => binomial n i * power i a).
proof: Proof. rewrite Newton_nat. apply msum_ext. intros; rewrite power_of_1; ring. Qed.
imports: List Arith ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list binomial)