proposition: Fact sum_power_lt k n f : k <> 0 -> (forall i, i < n -> f i < k) -> ∑ n (fun i => f i * power i k) < power n k.
proof: Proof. intros Hk. revert f; induction n as [ | n IHn ]; intros f Hf. + rewrite msum_0, power_0; lia. + rewrite msum_S, power_S, power_0, Nat.mul_1_r. apply Nat.le_trans with (k+ k * (power n k-1)). * apply (@Nat.add_le_mono (S (f 0))). - apply Hf; lia. - rewrite msum_ext with (g := fun i => k*(f (S i)*power i k)). ++ rewrite sum_0n_distr_l with (one := 1); auto; try (intros; ring). apply Nat.mul_le_mono_l. apply le_S_n, Nat.le_trans with (power n k); try lia. apply IHn; intros; apply Hf; lia. ++ intros; rewrite power_S; ring. * generalize (power_ge_1 n Hk); intros ?. replace (power n k) with (1+(power n k - 1)) at 2 by lia. rewrite Nat.mul_add_distr_l. apply Nat.add_le_mono; lia. Qed.
imports: List Arith ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list binomial)