fact: Fixpoint mset_to_poly (A: list nat) := match A with | [] => [] | a :: A => poly_add (repeat 0 a ++ [1]) (mset_to_poly A) end.
imports: List PeanoNat Lia Permutation Undecidability.SetConstraints.FMsetC Undecidability.PolynomialConstraints.LPolyNC Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun