proposition: Fact sum_0n_le_one n f i : i < n -> f i <= ∑ n f.
proof: Proof. revert f i; induction n as [ | n IHn ]; intros f i H. + lia. + rewrite msum_S. destruct i as [ | i ]; try lia. apply Nat.succ_lt_mono, IHn with (f := fun i => f (S i)) in H. lia. Qed.
imports: List Arith ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list binomial)