Theory Power_Sum_Polynomials_Library

(*
  File:     Power_Sum_Polynomials_Library.thy
  Author:   Manuel Eberl, TU München
*)
section ‹Auxiliary material›
theory Power_Sum_Polynomials_Library
imports
  "Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized"  
  "Symmetric_Polynomials.Symmetric_Polynomials"
  "HOL-Computational_Algebra.Computational_Algebra"
begin

unbundle multiset.lifting

subsection ‹Miscellaneous›

lemma atLeastAtMost_nat_numeral:
  "atLeastAtMost m (numeral k :: nat) =
     (if m ≤ numeral k then insert (numeral k) (atLeastAtMost m (pred_numeral k))
                 else {})"
  by (simp add: numeral_eq_Suc atLeastAtMostSuc_conv)

lemma sum_in_Rats [intro]: "(⋀x. x ∈ A ⟹ f x ∈ ℚ) ⟹ sum f A ∈ ℚ"
  by (induction A rule: infinite_finite_induct) auto

(* TODO Move *)
lemma (in monoid_mult) prod_list_distinct_conv_prod_set:
  "distinct xs ⟹ prod_list (map f xs) = prod f (set xs)"
  by (induct xs) simp_all

lemma (in monoid_mult) interv_prod_list_conv_prod_set_nat:
  "prod_list (map f [m..<n]) = prod f (set [m..<n])"
  by (simp add: prod_list_distinct_conv_prod_set)

lemma (in monoid_mult) prod_list_prod_nth:
  "prod_list xs = (∏i = 0..< length xs. xs ! i)"
  using interv_prod_list_conv_prod_set_nat [of "(!) xs" 0 "length xs"] by (simp add: map_nth)


lemma gcd_poly_code_aux_reduce:
  "gcd_poly_code_aux p 0 = normalize p"
  "q ≠ 0 ⟹ gcd_poly_code_aux p q = gcd_poly_code_aux q (primitive_part (pseudo_mod p q))"
  by (subst gcd_poly_code_aux.simps; simp)+

lemma coprimeI_primes:
  fixes a b :: "'a :: factorial_semiring"
  assumes "a ≠ 0 ∨ b ≠ 0"
  assumes "⋀p. prime p ⟹ p dvd a ⟹ p dvd b ⟹ False"
  shows   "coprime a b"
proof (rule coprimeI)
  fix d assume d: "d dvd a" "d dvd b"
  with assms(1) have [simp]: "d ≠ 0" by auto
  show "is_unit d"
  proof (rule ccontr)
    assume "¬is_unit d"
    then obtain p where p: "prime p" "p dvd d"
      using prime_divisor_exists[of d] by auto
    from assms(2)[of p] and p and d show False
      using dvd_trans by auto
  qed
qed

lemma coprime_pderiv_imp_squarefree:
  assumes "coprime p (pderiv p)"
  shows   "squarefree p"
proof (rule squarefreeI)
  fix d assume d: "d ^ 2 dvd p"
  then obtain q where q: "p = d ^ 2 * q"
    by (elim dvdE)
  hence "d dvd p" "d dvd pderiv p"
    by (auto simp: pderiv_mult pderiv_power_Suc numeral_2_eq_2)
  with assms show "is_unit d"
    using not_coprimeI by blast
qed

lemma squarefree_field_poly_iff:
  fixes p :: "'a :: {field_char_0,euclidean_ring_gcd,semiring_gcd_mult_normalize} poly"
  assumes [simp]: "p ≠ 0"
  shows "squarefree p ⟷ coprime p (pderiv p)"
proof
  assume "squarefree p"
  show "coprime p (pderiv p)"
  proof (rule coprimeI_primes)
    fix d assume d: "d dvd p" "d dvd pderiv p" "prime d"
    from d(1) obtain q where q: "p = d * q"
      by (elim dvdE)   
    from d(2) and q have "d dvd q * pderiv d"
      by (simp add: pderiv_mult dvd_add_right_iff)
    with ‹prime d› have "d dvd q ∨ d dvd pderiv d"
      using prime_dvd_mult_iff by blast
    thus False
    proof
      assume "d dvd q"
      hence "d ^ 2 dvd p"
        by (auto simp: q power2_eq_square)
      with ‹squarefree p› show False
        using d(3) not_prime_unit squarefreeD by blast
    next
      assume "d dvd pderiv d"
      hence "Polynomial.degree d = 0" by simp
      moreover have "d ≠ 0" using d by auto
      ultimately show False
        using d(3) is_unit_iff_degree not_prime_unit by blast
    qed
  qed auto
qed (use coprime_pderiv_imp_squarefree[of p] in auto)

lemma coprime_pderiv_imp_rsquarefree:
  assumes "coprime (p :: 'a :: field_char_0 poly) (pderiv p)"
  shows   "rsquarefree p"
  unfolding rsquarefree_roots
proof safe
  fix x assume "poly p x = 0" "poly (pderiv p) x = 0"
  hence "[:-x, 1:] dvd p" "[:-x, 1:] dvd pderiv p"
    by (auto simp: poly_eq_0_iff_dvd)
  with assms have "is_unit [:-x, 1:]"
    using not_coprimeI by blast
  thus False by auto
qed

lemma poly_of_nat [simp]: "poly (of_nat n) x = of_nat n"
  by (induction n) auto

lemma poly_of_int [simp]: "poly (of_int n) x = of_int n"
  by (cases n) auto

lemma order_eq_0_iff: "p ≠ 0 ⟹ order x p = 0 ⟷ poly p x ≠ 0"
  by (auto simp: order_root)

lemma order_pos_iff: "p ≠ 0 ⟹ order x p > 0 ⟷ poly p x = 0"
  by (auto simp: order_root)

lemma order_prod:
  assumes "⋀x. x ∈ A ⟹ f x ≠ 0"
  shows   "order x (∏y∈A. f y) = (∑y∈A. order x (f y))"
  using assms by (induction A rule: infinite_finite_induct) (auto simp: order_mult)

lemma order_prod_mset:
  assumes "0 ∉# A"
  shows   "order x (prod_mset A) = sum_mset (image_mset (order x) A)"
  using assms by (induction A) (auto simp: order_mult)

lemma order_prod_list:
  assumes "0 ∉ set xs"
  shows   "order x (prod_list xs) = sum_list (map (order x) xs)"
  using assms by (induction xs) (auto simp: order_mult)

lemma order_power: "p ≠ 0 ⟹ order x (p ^ n) = n * order x p"
  by (induction n) (auto simp: order_mult)


lemma smult_0_right [simp]: "MPoly_Type.smult p 0 = 0"
  by (transfer, transfer) auto

lemma mult_smult_right [simp]: 
  fixes c :: "'a :: comm_semiring_0"
  shows "p * MPoly_Type.smult c q = MPoly_Type.smult c (p * q)"
  by (simp add: smult_conv_mult mult_ac)

lemma mapping_single_eq_iff [simp]:
  "Poly_Mapping.single a b = Poly_Mapping.single c d ⟷ b = 0 ∧ d = 0 ∨ a = c ∧ b = d"
  by transfer (unfold fun_eq_iff when_def, metis)

lemma monom_of_set_plus_monom_of_set:
  assumes "A ∩ B = {}" "finite A" "finite B"
  shows   "monom_of_set A + monom_of_set B = monom_of_set (A ∪ B)"
  using assms by transfer (auto simp: fun_eq_iff)
  
lemma mpoly_monom_0_eq_Const: "monom 0 c = Const c"
  by (intro mpoly_eqI) (auto simp: coeff_monom when_def mpoly_coeff_Const)

lemma mpoly_Const_0 [simp]: "Const 0 = 0"
  by (intro mpoly_eqI) (auto simp: mpoly_coeff_Const mpoly_coeff_0)

lemma mpoly_Const_1 [simp]: "Const 1 = 1"
  by (intro mpoly_eqI) (auto simp: mpoly_coeff_Const mpoly_coeff_1)

lemma mpoly_Const_uminus: "Const (-a) = -Const a"
  by (intro mpoly_eqI) (auto simp: mpoly_coeff_Const)

lemma mpoly_Const_add: "Const (a + b) = Const a + Const b"
  by (intro mpoly_eqI) (auto simp: mpoly_coeff_Const)

lemma mpoly_Const_mult: "Const (a * b) = Const a * Const b"
  unfolding mpoly_monom_0_eq_Const [symmetric] mult_monom by simp

lemma mpoly_Const_power: "Const (a ^ n) = Const a ^ n"
  by (induction n) (auto simp: mpoly_Const_mult)

lemma of_nat_mpoly_eq: "of_nat n = Const (of_nat n)"
proof (induction n)
  case 0
  have "0 = (Const 0 :: 'a mpoly)"
    by (intro mpoly_eqI) (auto simp: mpoly_coeff_Const)
  thus ?case
    by simp
next
  case (Suc n)
  have "1 + Const (of_nat n) = Const (1 + of_nat n)"
    by (intro mpoly_eqI) (auto simp: mpoly_coeff_Const mpoly_coeff_1)
  thus ?case
    using Suc by auto
qed

lemma insertion_of_nat [simp]: "insertion f (of_nat n) = of_nat n"
  by (simp add: of_nat_mpoly_eq)
  
lemma insertion_monom_of_set [simp]:
  "insertion f (monom (monom_of_set X) c) = c * (∏i∈X. f i)"
proof (cases "finite X")
  case [simp]: True
  have "insertion f (monom (monom_of_set X) c) = c * (∏a. f a ^ (if a ∈ X then 1 else 0))"
    by (auto simp: lookup_monom_of_set)
  also have "(∏a. f a ^ (if a ∈ X then 1 else 0)) = (∏i∈X. f i ^ (if i ∈ X then 1 else 0))"
    by (intro Prod_any.expand_superset) auto
  also have "… = (∏i∈X. f i)"
    by (intro prod.cong) auto
  finally show ?thesis .
qed (auto simp: lookup_monom_of_set)


(* TODO: Move! Version in AFP is too weak! *)
lemma symmetric_mpoly_symmetric_sum:
  assumes "⋀π. π permutes A ⟹ g π permutes X"
  assumes "⋀x π. x ∈ X ⟹ π permutes A ⟹ mpoly_map_vars π (f x) = f (g π x)"
  shows "symmetric_mpoly A (∑x∈X. f x)"
  unfolding symmetric_mpoly_def
proof safe
  fix π assume π: "π permutes A"
  have "mpoly_map_vars π (sum f X) = (∑x∈X. mpoly_map_vars π (f x))"
    by simp
  also have "… = (∑x∈X. f (g π x))"
    by (intro sum.cong assms π refl)
  also have "… = (∑x∈g π`X. f x)"
    using assms(1)[OF π] by (subst sum.reindex) (auto simp: permutes_inj_on)
  also have "g π ` X = X"
    using assms(1)[OF π] by (simp add: permutes_image)
  finally show "mpoly_map_vars π (sum f X) = sum f X" .
qed

lemma sym_mpoly_0 [simp]:
  assumes "finite A"
  shows   "sym_mpoly A 0 = 1"
  using assms by (transfer, transfer) (auto simp: fun_eq_iff when_def)

lemma sym_mpoly_eq_0 [simp]:
  assumes "k > card A"
  shows   "sym_mpoly A k = 0"
proof (transfer fixing: A k, transfer fixing: A k, intro ext)
  fix mon
  have "¬(finite A ∧ (∃Y⊆A. card Y = k ∧ mon = monom_of_set Y))"
  proof safe
    fix Y assume Y: "finite A" "Y ⊆ A" "k = card Y" "mon = monom_of_set Y"
    hence "card Y ≤ card A" by (intro card_mono) auto
    with Y and assms show False by simp
  qed
  thus "(if finite A ∧ (∃Y⊆A. card Y = k ∧ mon = monom_of_set Y) then 1 else 0) = 0"
    by auto
qed

lemma coeff_sym_mpoly_monom_of_set_eq_0:
  assumes "finite X" "Y ⊆ X" "card Y ≠ k"
  shows   "MPoly_Type.coeff (sym_mpoly X k) (monom_of_set Y) = 0"
  using assms finite_subset[of _ X] by (auto simp: coeff_sym_mpoly)

lemma coeff_sym_mpoly_monom_of_set_eq_0':
  assumes "finite X" "¬Y ⊆ X" "finite Y"
  shows   "MPoly_Type.coeff (sym_mpoly X k) (monom_of_set Y) = 0"
  using assms finite_subset[of _ X] by (auto simp: coeff_sym_mpoly)


subsection ‹The set of roots of a univariate polynomial›

lift_definition poly_roots :: "'a :: idom poly ⇒ 'a multiset" is
  "λp x. if p = 0 then 0 else order x p"
proof -
  fix p :: "'a poly"
  show "finite {x. 0 < (if p = 0 then 0 else order x p)}"
    by (cases "p = 0") (auto simp: order_pos_iff poly_roots_finite)
qed

lemma poly_roots_0 [simp]: "poly_roots 0 = {#}"
  by transfer auto

lemma poly_roots_1 [simp]: "poly_roots 1 = {#}"
  by transfer auto

lemma count_poly_roots [simp]:
  assumes "p ≠ 0"
  shows   "count (poly_roots p) x = order x p"
  using assms by transfer auto

lemma in_poly_roots_iff [simp]: "p ≠ 0 ⟹ x ∈# poly_roots p ⟷ poly p x = 0"
  by (subst count_greater_zero_iff [symmetric], subst count_poly_roots) (auto simp: order_pos_iff)

lemma set_mset_poly_roots: "p ≠ 0 ⟹ set_mset (poly_roots p) = {x. poly p x = 0}"
  using in_poly_roots_iff[of p] by blast

lemma count_poly_roots': "count (poly_roots p) x = (if p = 0 then 0 else order x p)"
  by transfer' auto

lemma poly_roots_const [simp]: "poly_roots [:c:] = {#}"
  by (intro multiset_eqI) (auto simp: count_poly_roots' order_eq_0_iff)

lemma poly_roots_linear [simp]: "poly_roots [:-x, 1:] = {#x#}"
  by (intro multiset_eqI) (auto simp: count_poly_roots' order_eq_0_iff)

lemma poly_roots_monom [simp]: "c ≠ 0 ⟹ poly_roots (Polynomial.monom c n) = replicate_mset n 0"
  by (intro multiset_eqI) (auto simp: count_poly_roots' order_eq_0_iff poly_monom)

lemma poly_roots_smult [simp]: "c ≠ 0 ⟹ poly_roots (Polynomial.smult c p) = poly_roots p"
  by (intro multiset_eqI) (auto simp: count_poly_roots' order_smult)

lemma poly_roots_mult: "p ≠ 0 ⟹ q ≠ 0 ⟹ poly_roots (p * q) = poly_roots p + poly_roots q"
  by (intro multiset_eqI) (auto simp: count_poly_roots' order_mult)

lemma poly_roots_prod:
  assumes "⋀x. x ∈ A ⟹ f x ≠ 0"
  shows   "poly_roots (prod f A) = (∑x∈A. poly_roots (f x))"
  using assms by (induction A rule: infinite_finite_induct) (auto simp: poly_roots_mult)

lemma poly_roots_prod_mset:
  assumes "0 ∉# A"
  shows   "poly_roots (prod_mset A) = sum_mset (image_mset poly_roots A)"
  using assms by (induction A) (auto simp: poly_roots_mult)

lemma poly_roots_prod_list:
  assumes "0 ∉ set xs"
  shows   "poly_roots (prod_list xs) = sum_list (map poly_roots xs)"
  using assms by (induction xs) (auto simp: poly_roots_mult)

lemma poly_roots_power: "p ≠ 0 ⟹ poly_roots (p ^ n) = repeat_mset n (poly_roots p)"
  by (induction n) (auto simp: poly_roots_mult)

lemma rsquarefree_poly_roots_eq:
  assumes "rsquarefree p"
  shows   "poly_roots p = mset_set {x. poly p x = 0}"
proof (rule multiset_eqI)
  fix x :: 'a
  from assms show "count (poly_roots p) x = count (mset_set {x. poly p x = 0}) x"
    by (cases "poly p x = 0") (auto simp: poly_roots_finite order_eq_0_iff rsquarefree_def)
qed

lemma rsquarefree_imp_distinct_roots:
  assumes "rsquarefree p" and "mset xs = poly_roots p"
  shows   "distinct xs"
proof (cases "p = 0")
  case [simp]: False
  have *: "mset xs = mset_set {x. poly p x = 0}"
    using assms by (simp add: rsquarefree_poly_roots_eq)
  hence "set_mset (mset xs) = set_mset (mset_set {x. poly p x = 0})"
    by (simp only: )
  hence [simp]: "set xs = {x. poly p x = 0}"
    by (simp add: poly_roots_finite)
  from * show ?thesis
    by (subst distinct_count_atmost_1) (auto simp: poly_roots_finite)
qed (use assms in auto)

lemma poly_roots_factorization:
  fixes p c A
  assumes [simp]: "c ≠ 0"
  defines "p ≡ Polynomial.smult c (prod_mset (image_mset (λx. [:-x, 1:]) A))"
  shows   "poly_roots p = A"
proof -
  have "poly_roots p = poly_roots (∏x∈#A. [:-x, 1:])"
    by (auto simp: p_def)
  also have "… = A"
    by (subst poly_roots_prod_mset) (auto simp: image_mset.compositionality o_def)
  finally show ?thesis .
qed

lemma fundamental_theorem_algebra_factorized':
  fixes p :: "complex poly"
  shows "p = Polynomial.smult (Polynomial.lead_coeff p) 
               (prod_mset (image_mset (λx. [:-x, 1:]) (poly_roots p)))"
proof (cases "p = 0")
  case [simp]: False
  obtain xs where
    xs: "Polynomial.smult (Polynomial.lead_coeff p) (∏x←xs. [:-x, 1:]) = p"
        "length xs = Polynomial.degree p"
    using fundamental_theorem_algebra_factorized[of p] by auto
  define A where "A = mset xs"

  note xs(1)
  also have "(∏x←xs. [:-x, 1:]) = prod_mset (image_mset (λx. [:-x, 1:]) A)"
    unfolding A_def by (induction xs) auto
  finally have *: "Polynomial.smult (Polynomial.lead_coeff p) (∏x∈#A. [:- x, 1:]) = p" .
  also have "A = poly_roots p"
    using poly_roots_factorization[of "Polynomial.lead_coeff p" A]
    by (subst * [symmetric]) auto
  finally show ?thesis ..
qed auto
  
lemma poly_roots_eq_imp_eq:
  fixes p q :: "complex poly"
  assumes "Polynomial.lead_coeff p = Polynomial.lead_coeff q"
  assumes "poly_roots p = poly_roots q"
  shows   "p = q"
proof (cases "p = 0 ∨ q = 0")
  case False
  hence [simp]: "p ≠ 0" "q ≠ 0"
    by auto
  have "p = Polynomial.smult (Polynomial.lead_coeff p) 
               (prod_mset (image_mset (λx. [:-x, 1:]) (poly_roots p)))"
    by (rule fundamental_theorem_algebra_factorized')
  also have "… = Polynomial.smult (Polynomial.lead_coeff q) 
                   (prod_mset (image_mset (λx. [:-x, 1:]) (poly_roots q)))"
    by (simp add: assms)
  also have "… = q"
    by (rule fundamental_theorem_algebra_factorized' [symmetric])
  finally show ?thesis .
qed (use assms in auto)

lemma Sum_any_zeroI': "(⋀x. P x ⟹ f x = 0) ⟹ Sum_any (λx. f x when P x) = 0"
  by (auto simp: Sum_any.expand_set)

(* TODO: This was not really needed here, but it is important nonetheless.
   It should go in the Symmetric_Polynomials entry. *)
lemma sym_mpoly_insert:
  assumes "finite X" "x ∉ X"
  shows   "(sym_mpoly (insert x X) (Suc k) :: 'a :: semiring_1 mpoly) =
             monom (monom_of_set {x}) 1 * sym_mpoly X k + sym_mpoly X (Suc k)" (is "?lhs = ?A + ?B")
proof (rule mpoly_eqI)
  fix mon
  show "coeff ?lhs mon = coeff (?A + ?B) mon"
  proof (cases "∀i. lookup mon i ≤ 1 ∧ (i ∉ insert x X ⟶ lookup mon i = 0)")
    case False
    then obtain i where i: "lookup mon i > 1 ∨ i ∉ insert x X ∧ lookup mon i > 0"
      by (auto simp: not_le)
    
    have "coeff ?A mon = prod_fun (coeff (monom (monom_of_set {x}) 1))
                                  (coeff (sym_mpoly X k)) mon"
      by (simp add: coeff_mpoly_times)
    also have "… = (∑l. ∑q. coeff (monom (monom_of_set {x}) 1) l * coeff (sym_mpoly X k) q
                         when mon = l + q)"
        unfolding prod_fun_def 
        by (intro Sum_any.cong, subst Sum_any_right_distrib, force)
           (auto simp: Sum_any_right_distrib when_def intro!: Sum_any.cong)
    also have "… = 0"
    proof (rule Sum_any_zeroI, rule Sum_any_zeroI')
      fix ma mb assume *: "mon = ma + mb"
      show "coeff (monom (monom_of_set {x}) (1::'a)) ma * coeff (sym_mpoly X k) mb = 0"
      proof (cases "i = x")
        case [simp]: True
        show ?thesis
        proof (cases "lookup mb i > 0")
          case True
          hence "coeff (sym_mpoly X k) mb = 0" using ‹x ∉ X›
            by (auto simp: coeff_sym_mpoly lookup_monom_of_set split: if_splits)
          thus ?thesis
            using mult_not_zero by blast
        next
          case False
          hence "coeff (monom (monom_of_set {x}) 1) ma = 0"
            using i by (auto simp: coeff_monom when_def * lookup_add)
          thus ?thesis
            using mult_not_zero by blast
        qed
      next
        case [simp]: False
        show ?thesis
        proof (cases "lookup ma i > 0")
          case False
          hence "lookup mb i = lookup mon i"
            using * by (auto simp: lookup_add)
          hence "coeff (sym_mpoly X k) mb = 0" using i
            by (auto simp: coeff_sym_mpoly lookup_monom_of_set split: if_splits)
          thus ?thesis
            using mult_not_zero by blast
        next
          case True
          hence "coeff (monom (monom_of_set {x}) 1) ma = 0"
            using i by (auto simp: coeff_monom when_def * lookup_add)
          thus ?thesis
            using mult_not_zero by blast
        qed
      qed
    qed
    finally have "coeff ?A mon = 0" .
    moreover from False have "coeff ?lhs mon = 0"
      by (subst coeff_sym_mpoly) (auto simp: lookup_monom_of_set split: if_splits)
    moreover from False have "coeff (sym_mpoly X (Suc k)) mon = 0"
      by (subst coeff_sym_mpoly) (auto simp: lookup_monom_of_set split: if_splits)
    ultimately show ?thesis
      by auto
  next
    case True
    define A where "A = keys mon"
    have A: "A ⊆ insert x X"
      using True by (auto simp: A_def)
    have [simp]: "mon = monom_of_set A"
      unfolding A_def using True by transfer (force simp: fun_eq_iff le_Suc_eq)
    have "finite A"
      using finite_subset A assms by blast
    show ?thesis
    proof (cases "x ∈ A")
      case False
      have "coeff ?A mon = prod_fun (coeff (monom (monom_of_set {x}) 1))
                                    (coeff (sym_mpoly X k)) (monom_of_set A)"
        by (simp add: coeff_mpoly_times)
      also have "… = (∑l. ∑q. coeff (monom (monom_of_set {x}) 1) l * coeff (sym_mpoly X k) q
                         when monom_of_set A = l + q)"
        unfolding prod_fun_def 
        by (intro Sum_any.cong, subst Sum_any_right_distrib, force)
           (auto simp: Sum_any_right_distrib when_def intro!: Sum_any.cong)
      also have "… = 0"
      proof (rule Sum_any_zeroI, rule Sum_any_zeroI')
        fix ma mb assume *: "monom_of_set A = ma + mb"
        hence "keys ma ⊆ A"
          using ‹finite A› by transfer (auto simp: fun_eq_iff split: if_splits)
        thus "coeff (monom (monom_of_set {x}) (1::'a)) ma * coeff (sym_mpoly X k) mb = 0"
          using ‹x ∉ A› by (auto simp: coeff_monom when_def)
      qed
      finally show ?thesis
        using False A assms finite_subset[of _ "insert x X"] finite_subset[of _ X]
        by (auto simp: coeff_sym_mpoly)
    next
      case True
      have "mon = monom_of_set {x} + monom_of_set (A - {x})"
        using ‹x ∈ A› ‹finite A› by (auto simp: monom_of_set_plus_monom_of_set)
      also have "coeff ?A … = coeff (sym_mpoly X k) (monom_of_set (A - {x}))"
        by (subst coeff_monom_mult) auto
      also have "… = (if card A = Suc k then 1 else 0)"
      proof (cases "card A = Suc k")
        case True
        thus ?thesis
          using assms ‹finite A› ‹x ∈ A› A
          by (subst coeff_sym_mpoly_monom_of_set) auto
      next
        case False
        thus ?thesis
          using assms ‹x ∈ A› A ‹finite A› card_Suc_Diff1[of A x]
          by (subst coeff_sym_mpoly_monom_of_set_eq_0) auto
      qed
      moreover have "coeff ?B (monom_of_set A) = 0"
        using assms ‹x ∈ A› ‹finite A›
        by (subst coeff_sym_mpoly_monom_of_set_eq_0') auto
      moreover have "coeff ?lhs (monom_of_set A) = (if card A = Suc k then 1 else 0)"
        using assms A ‹finite A› finite_subset[of _ "insert x X"] by (auto simp: coeff_sym_mpoly)
      ultimately show ?thesis by simp
    qed
  qed
qed

lifting_update multiset.lifting
lifting_forget multiset.lifting

end