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