proposition: Fact msum_first_two n f : 2 <= n -> (forall i, 2 <= i -> f i = u) -> ∑ n f = f 0 ⊕ f 1.
proof: Proof. Proof using Hmonoid. destruct Hmonoid as [ _ M2 _ ]. intros Hn H1. destruct n as [ | [ | n ] ]; try lia. do 2 rewrite msum_S. rewrite msum_of_unit. + rewrite M2; trivial. + intros; apply H1; lia. Qed.
imports: List Arith ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list binomial)