proposition: Fact sum_0n_mono n f g : (forall i, i < n -> f i <= g i) -> ∑ n f <= ∑ n g.
proof: Proof. revert f g; induction n as [ | n IHn ]; intros f g H. + do 2 rewrite msum_0; auto. + do 2 rewrite msum_S; apply Nat.add_le_mono. * apply H; lia. * apply IHn; intros; apply H; lia. Qed.
imports: List Arith ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list binomial)