proposition: Lemma mset_to_poly_eqI {A B} : A ≡ B -> mset_to_poly A ≃ mset_to_poly B.
proof: Proof. move=> /Permutation_count_occ. elim: A B. - by move=> B /Permutation_nil ->. - move=> a A IH B /[dup] /(Permutation_in a) /(_ (in_eq _ _)). move=> /(@in_split nat) [B1 [B2 ->]] /(@Permutation_cons_app_inv nat) /IH {}IH i. move: (IH i) (@mset_to_poly_shift a B1 B2 i). rewrite /= !poly_add_nthP. by lia. Qed.
imports: List PeanoNat Lia Permutation Undecidability.SetConstraints.FMsetC Undecidability.PolynomialConstraints.LPolyNC Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun