proposition: Lemma mset_to_poly_mapP {A} : mset_to_poly (map S A) ≃ 0 :: mset_to_poly A.
proof: Proof. elim: A; first by (case; [done | by case]). move=> a A + i => /(_ i). case: i. - by rewrite /map -/(map _ _) ?poly_add_nthP. - move=> i. rewrite /map -/(map _ _) /mset_to_poly -/(mset_to_poly). rewrite /= ?poly_add_nthP /=. by lia. Qed.
imports: List PeanoNat Lia Permutation Undecidability.SetConstraints.FMsetC Undecidability.PolynomialConstraints.LPolyNC Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun