proposition: Lemma poly_to_mset_consP {p} : poly_to_mset (0 :: p) = map S (poly_to_mset p).
proof: Proof. done. Qed.
imports: List PeanoNat Lia Permutation Undecidability.SetConstraints.FMsetC Undecidability.PolynomialConstraints.LPolyNC Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun