proposition: Fact msum_only_one n f i : i < n -> (forall j, j < n -> i <> j -> f j = u) -> ∑ n f = f i.
proof: Proof. Proof using Hmonoid. destruct Hmonoid as [ M1 M2 M3 ]. intros H1 H2. replace n with (i + 1 + (n-i-1)) by lia. do 2 rewrite msum_plus. rewrite msum_of_unit, msum_1, msum_of_unit, M1, M2. + f_equal; lia. + intros j Hj; destruct (H2 (i+1+j)); auto; lia. + intros j Hj; destruct (H2 j); auto; lia. Qed.
imports: List Arith ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list binomial)