proposition: Fact msum_comm a n f : (forall i, i < n -> f i ⊕ a = a ⊕ f i) -> ∑ n f ⊕ a = a ⊕ ∑ n f.
proof: Proof. Proof using Hmonoid. destruct Hmonoid as [ H1 H2 H3 ]. revert f; induction n as [ | n IHn ]; intros f H; simpl; auto. + rewrite H1, H2; auto. + rewrite H3, <- H; try lia. repeat rewrite <- H3; f_equal. apply IHn. intros; apply H; lia. Qed.
imports: List Arith ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list binomial)