fact: Record monoid_theory (X : Type) (m : X -> X -> X) (u : X) := mk_monoid { monoid_unit_l : forall x, m u x = x; monoid_unit_r : forall x, m x u = x; monoid_assoc : forall x y z, m x (m y z) = m (m x y) z; }.
imports: List Arith ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list binomial)