proposition: Lemma count_occ_poly_to_msetP {a p}: count_occ Nat.eq_dec (poly_to_mset p) a = nth a p 0.
proof: Proof. elim: a p. - case; first done. move=> + p /=. elim; first by elim: (poly_to_mset p). by move=> ? /= ->. - move=> i IH. case; first done. move=> a p /=. rewrite count_occ_app. rewrite -(count_occ_map S Nat.eq_dec) ?IH; first by lia. by elim a. Qed.
imports: List PeanoNat Lia Permutation Undecidability.SetConstraints.FMsetC Undecidability.PolynomialConstraints.LPolyNC Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun