Theory Card_Number_Partitions.Number_Partition

(*  Author: Lukas Bulwahn <lukas.bulwahn-at-gmail.com> *)

section ‹Number Partitions›

theory Number_Partition
imports Additions_to_Main
begin

subsection ‹Number Partitions as @{typ "nat => nat"} Functions›

definition partitions :: "(nat ⇒ nat) ⇒ nat ⇒ bool" (infix ‹partitions› 50)
where
  "p partitions n = ((∀i. p i ≠ 0 ⟶ 1 ≤ i ∧ i ≤ n) ∧ (∑i≤n. p i * i) = n)"

lemma partitionsI:
  assumes "⋀i. p i ≠ 0 ⟹ 1 ≤ i ∧ i ≤ n"
  assumes "(∑i≤n. p i * i) = n"
  shows "p partitions n"
using assms unfolding partitions_def by auto

lemma partitionsE:
  assumes "p partitions n"
  obtains "⋀i. p i ≠ 0 ⟹ 1 ≤ i ∧ i ≤ n" "(∑i≤n. p i * i) = n"
using assms unfolding partitions_def by auto

lemma partitions_zero:
  "p partitions 0 ⟷ p = (λi. 0)"
unfolding partitions_def by auto

lemma partitions_one:
  "p partitions (Suc 0) ⟷ p = (λi. 0)(1 := 1)"
unfolding partitions_def
by (auto split: if_split_asm) (auto simp add: fun_eq_iff)

subsection ‹Bounds and Finiteness of Number Partitions›

lemma partitions_imp_finite_elements:
  assumes "p partitions n"
  shows "finite {i. 0 < p i}"
proof -
  from assms have "{i. 0 < p i} ⊆ {..n}" by (auto elim: partitionsE)
  from this show ?thesis
    using rev_finite_subset by blast
qed

lemma partitions_bounds:
  assumes "p partitions n"
  shows "p i ≤ n"
proof -
  from assms have index_bounds: "(∀i. p i ≠ 0 ⟶ 1 ≤ i ∧ i ≤ n)"
    and sum: "(∑i≤n. p i * i) = n"
    unfolding partitions_def by auto
  show ?thesis
  proof (cases "1 ≤ i ∧ i ≤ n")
    case True
    from True have "{..n} = insert i {i'. i' ≤ n ∧ i' ≠ i}" by blast
    from sum[unfolded this] have "p i * i + (∑i∈{i'. i' ≤ n ∧ i' ≠ i}. p i * i) = n" by auto
    from this have "p i * i ≤ n" by linarith
    from this True show ?thesis using dual_order.trans by fastforce
  next
    case False
    from this index_bounds show ?thesis by fastforce
  qed
qed

lemma partitions_parts_bounded:
  assumes "p partitions n"
  shows "sum p {..n} ≤ n"
proof -
  {
    fix i
    assume "i ≤ n"
    from assms have "p i ≤ p i * i"
      by (auto elim!: partitionsE)
  }
  from this have "sum p {..n} ≤ (∑i≤n. p i * i)"
    by (auto intro: sum_mono)
  also from assms have n: "(∑i≤n. p i * i) = n"
    by (auto elim!: partitionsE)
  finally show ?thesis .
qed

lemma finite_partitions:
  "finite {p. p partitions n}"
proof -
  have "{p. p partitions n} ⊆ {f. (∀i. f i ≤ n) ∧ (∀i. n + 1 ≤ i ⟶ f i = 0)}"
    by (auto elim: partitions_bounds) (auto simp add: partitions_def)
  from this bound_domain_and_range_impl_finitely_many_functions[of n "n + 1"] show ?thesis
    by (simp add: finite_subset)
qed

lemma finite_partitions_k_parts:
  "finite {p. p partitions n ∧ sum p {..n} = k}"
by (simp add: finite_partitions)

lemma partitions_remaining_Max_part:
  assumes "p partitions n"
  assumes "0 < p k"
  shows "∀i. n - k < i ∧ i ≠ k ⟶ p i = 0"
proof (clarify)
  fix i
  assume "n - k < i" "i ≠ k"
  show "p i = 0"
  proof (cases "i ≤ n")
    assume "i ≤ n"
    from assms have n: "(∑i≤n. p i * i) = n" and "k ≤ n"
      by (auto elim: partitionsE)
    have "(∑i≤n. p i * i) = p k * k + (∑i∈{..n}-{k}. p i * i)"
      using ‹k ≤ n› sum_atMost_remove_nat by blast
    also have "... = p i * i + p k * k + (∑i∈{..n}-{i, k}. p i * i)"
      using ‹i ≤ n› ‹i ≠ k›
      by (auto simp add: sum.remove[where x="i"]) (metis Diff_insert)
    finally have eq: "(∑i≤n. p i * i) = p i * i + p k * k + (∑i∈{..n} - {i, k}. p i * i)" .
    show "p i = 0"
    proof (rule ccontr)
      assume "p i ≠ 0"
      have upper_bound: "p i * i + p k * k ≤ n"
        using eq n by auto
      have lower_bound: "p i * i + p k * k > n"
        using ‹n - k < i› ‹0 < p k› ‹k ≤ n› ‹p i ≠ 0› mult_eq_if not_less by auto
      from upper_bound lower_bound show False by simp
    qed
  next
    assume "¬ (i ≤ n)"
    from this show "p i = 0"
      using assms(1) by (auto elim: partitionsE)
  qed
qed

subsection ‹Operations of Number Partitions›

lemma partitions_remove1_bounds:
  assumes partitions: "p partitions n"
  assumes gr0: "0 < p k"
  assumes neq: "(p(k := p k - 1)) i ≠ 0"
  shows "1 ≤ i ∧ i ≤ n - k"
proof
    from partitions neq show "1 ≤ i"
      by (auto elim!: partitionsE split: if_split_asm)
next
  from partitions gr0 have n: "(∑i≤n. p i * i) = n" and "k ≤ n"
    by (auto elim: partitionsE)
  show "i ≤ n - k"
  proof cases
    assume "k ≤ n - k"
    from ‹k ≤ n - k› neq show ?thesis
      using  partitions_remaining_Max_part[OF partitions gr0] not_le by force
  next
    assume "¬ k ≤ n - k"
    from this have "2 * k > n" by auto
    have "p k = 1"
    proof (rule ccontr)
      assume "p k ≠ 1"
      with gr0 have "p k ≥ 2" by auto
      from this have "p k * k ≥ 2 * k" by simp
      with ‹2 * k > n› have "p k * k > n" by linarith
      from ‹k ≤ n› this have "(∑i≤n. p i * i) > n"
        by (simp add: sum_atMost_remove_nat[of k])
      from this n show "False" by auto
    qed
    from neq this show ?thesis
      using partitions_remaining_Max_part[OF partitions gr0] leI
      by (auto split: if_split_asm) force
  qed
qed

lemma partitions_remove1:
  assumes partitions: "p partitions n"
  assumes gr0: "0 < p k"
  shows "p(k := p k - 1) partitions (n - k)"
proof (rule partitionsI)
  fix i
  assume "(p(k := p k - 1)) i ≠ 0"
  from this show "1 ≤ i ∧ i ≤ n - k" using partitions_remove1_bounds partitions gr0 by blast
next
  from partitions gr0 have "k ≤ n" by (auto elim: partitionsE)
  have "(∑i≤n - k. (p(k := p k - 1)) i * i) = (∑i≤n. (p(k := p k - 1)) i * i)"
    using partitions_remove1_bounds partitions gr0 by (auto intro!: sum.mono_neutral_left)
  also have "... = (p k - 1) * k + (∑i∈{..n} - {k}. (p(k := p k - 1)) i * i)"
    using ‹k ≤ n› by (simp add: sum_atMost_remove_nat[where k="k"])
  also have "... = p k * k + (∑i∈{..n} - {k}. p i * i) - k"
    using gr0 by (simp add: diff_mult_distrib)
  also have "... = (∑i≤n. p i * i) - k"
    using ‹k ≤ n› by (simp add: sum_atMost_remove_nat[of k])
  also from partitions have "... = n - k"
    by (auto elim: partitionsE)
  finally show "(∑i≤n - k. (p(k := p k - 1)) i * i) = n - k" .
qed

lemma partitions_insert1:
  assumes p: "p partitions n"
  assumes "k > 0"
  shows "(p(k := p k + 1)) partitions (n + k)"
proof (rule partitionsI)
  fix i
  assume "(p(k := p k + 1)) i ≠ 0"
  from p this ‹k > 0› show "1 ≤ i ∧ i ≤ n + k"
    by (auto elim!: partitionsE)
next
  have "(∑i≤n + k. (p(k := p k + 1)) i * i) = p k * k + (∑i∈{..n + k} - {k}. p i * i) + k"
    by (simp add: sum_atMost_remove_nat[of k])
  also have "... = p k * k + (∑i∈{..n} - {k}. p i * i) + k"
    using p by (auto intro!: sum.mono_neutral_right elim!: partitionsE)
  also have "... = (∑i≤n. p i * i) + k"
    using p by (cases "k ≤ n") (auto simp add: sum_atMost_remove_nat[of k] elim: partitionsE)
  also have "... = n + k"
    using p by (auto elim: partitionsE)
  finally show "(∑i≤n + k. (p(k := p k + 1)) i * i) = n + k" .
qed

lemma count_remove1:
  assumes "p partitions n"
  assumes "0 < p k"
  shows "(∑i≤n - k. (p(k := p k - 1)) i) = (∑i≤n. p i) - 1"
proof -
  have "k ≤ n" using assms by (auto elim: partitionsE)
  have "(∑i≤n - k. (p(k := p k - 1)) i) = (∑i≤n. (p(k := p k - 1)) i)"
    using partitions_remove1_bounds assms by (auto intro!: sum.mono_neutral_left)
  also have "(∑i≤n. (p(k := p k - 1)) i) = p k + (∑i∈{..n} - {k}. p i) - 1"
    using ‹0 < p k› ‹k ≤ n› by (simp add: sum_atMost_remove_nat[of k])
  also have "... = (∑i∈{..n}. p i) - 1"
    using ‹k ≤ n› by (simp add: sum_atMost_remove_nat[of k])
  finally show ?thesis .
qed

lemma count_insert1:
  assumes "p partitions n"
  shows "sum (p(k := p k + 1)) {..n + k} = (∑i≤n. p i) + 1"
proof -
  have "(∑i≤n + k. (p(k := p k + 1)) i) = p k + (∑i∈{..n + k} - {k}. p i) + 1"
    by (simp add: sum_atMost_remove_nat[of k])
  also have "... = p k + (∑i∈{..n} - {k}. p i) + 1"
    using assms by (auto intro!: sum.mono_neutral_right elim!: partitionsE)
  also have "... = (∑i≤n. p i) + 1"
    using assms by (cases "k ≤ n") (auto simp add: sum_atMost_remove_nat[of k] elim: partitionsE)
  finally show ?thesis .
qed

lemma partitions_decrease1:
  assumes p: "p partitions m"
  assumes sum: "sum p {..m} = k"
  assumes "p 1 = 0"
  shows "(λi. p (i + 1)) partitions m - k"
proof -
  from p have "p 0 = 0" by (auto elim!: partitionsE)
  {
    fix i
    assume neq: "p (i + 1) ≠ 0"
    from p this ‹p 1 = 0› have "1 ≤ i"
      by (fastforce elim!: partitionsE simp add: le_Suc_eq)
    moreover have "i ≤ m - k"
    proof (rule ccontr)
      assume i_greater: "¬ i ≤ m - k"
      from p have s: "(∑i≤m. p i * i) = m"
        by (auto elim!: partitionsE)
      from p sum have "k ≤ m"
        using partitions_parts_bounded by fastforce
      from neq p have "i + 1 ≤ m" by (auto elim!: partitionsE)
      from i_greater have "i > m - k" by simp
      have ineq1: "i + 1 > (m - k) + 1"
        using i_greater by simp
      have ineq21: "(∑j≤m. (p(i + 1 := p (i + 1) - 1)) j * j) ≥ (∑j≤m. (p(i + 1 := p (i + 1) - 1)) j)"
        using ‹p 0 = 0› not_less by (fastforce intro!: sum_mono)
      have ineq22a: "(∑j≤m. (p(i + 1 := p (i + 1) - 1)) j) = (∑j≤m. p j) - 1"
        using ‹i + 1 ≤ m› neq by (simp add: sum.remove[where x="i + 1"])
      have ineq22: "(∑j≤m. (p(i + 1 := p (i + 1) - 1)) j) ≥ k - 1"
        using sum neq ineq22a by auto
      have ineq2: "(∑j≤m. (p(i + 1 := p (i + 1) - 1)) j * j) ≥ k - 1"
        using ineq21 ineq22 by auto
      have "(∑i≤m. p i * i) = p (i + 1) * (i + 1) + (∑i∈{..m} - {i + 1}. p i * i)"
        using ‹i + 1 ≤ m› neq
        by (subst sum.remove[where x="i + 1"]) auto
      also have "... = (i + 1) + (∑j≤m. (p(i + 1 := p (i + 1) - 1)) j * j)"
        using ‹i + 1 ≤ m› neq
        by (subst sum.remove[where x="i + 1" and g="λj. (p(i + 1 := p (i + 1) - 1)) j * j"])
          (auto simp add: mult_eq_if)
      finally have "(∑i≤m. p i * i) = i + 1 + (∑j≤m. (p(i + 1 := p (i + 1) - 1)) j * j)" .
      moreover have "... > m" using ineq1 ineq2 ‹k ≤ m› ‹p (i + 1) ≠ 0› by linarith
      ultimately have "(∑i≤m. p i * i) > m" by simp
      from s this show False by simp
    qed
    ultimately have "1 ≤ i ∧ i ≤ m - k" ..
  } note bounds = this
  show "(λi. p (i + 1)) partitions m - k"
  proof (rule partitionsI)
    fix i
    assume "p (i + 1) ≠ 0"
    from bounds this show "1 ≤ i ∧ i ≤ m - k" .
  next
    have geq: "∀i. p i * i ≥ p i"
      using ‹p 0 = 0› not_less by fastforce
    have "(∑i≤m - k. p (i + 1) * i) = (∑i≤m. p (i + 1) * i)"
      using bounds by (auto intro: sum.mono_neutral_left)
    also have "... = (∑i∈Suc ` {..m}. p i * (i - 1))"
      by (auto simp add: sum.reindex)
    also have "... = (∑i≤Suc m. p i * (i - 1))"
      using ‹p 0 = 0›
      by (simp add: atMost_Suc_eq_insert_0)
    also have "... = (∑i≤m. p i * (i - 1))"
      using p by (auto elim!: partitionsE)
    also have "... = (∑i≤m. p i * i - p i)"
      by (simp add: diff_mult_distrib2)
    also have "... = (∑i≤m. p i * i) - (∑i≤m. p i)"
      using geq by (simp only: sum_subtractf_nat)
    also have "... = m - k" using sum p by (auto elim!: partitionsE)
    finally show "(∑i≤m - k. p (i + 1) * i) = m - k" .
  qed
qed

lemma partitions_increase1:
  assumes partitions: "p partitions m - k"
  assumes k: "sum p {..m - k} = k"
  shows "(λi. p (i - 1)) partitions m"
proof (rule partitionsI)
  fix i
  assume "p (i - 1) ≠ 0"
  from partitions this k show "1 ≤ i ∧ i ≤ m"
    by (cases k) (auto elim!: partitionsE)
next
  from k partitions have "k ≤ m"
    using linear partitions_zero by force
  have eq_0: "∀i>m - k. p i = 0" using partitions by (auto elim!: partitionsE)
  from partitions have s: "(∑i≤m - k. p i * i) = m - k" by (auto elim!: partitionsE)
  have "(∑i≤m. p (i - 1) * i) = (∑i≤Suc m. p (i - 1) * i)"
    using partitions k by (cases k) (auto elim!: partitionsE)
  also have "(∑i≤Suc m. p (i - 1) * i) = (∑i≤m. p i * (i + 1))"
    by (subst sum.atMost_Suc_shift) simp
  also have "... = (∑i≤m - k. p i * (i + 1))"
    using eq_0 by (auto intro: sum.mono_neutral_right)
  also have "... = (∑i≤m - k. p i * i) + (∑i≤m - k. p i)" by (simp add: sum.distrib)
  also have "... = m - k + k" using s k by simp
  also have "... = m" using ‹k ≤ m› by simp
  finally show "(∑i≤m. p (i - 1) * i) = m" .
qed

lemma count_decrease1:
  assumes p: "p partitions m"
  assumes sum: "sum p {..m} = k"
  assumes "p 1 = 0"
  shows "sum (λi. p (i + 1)) {..m - k} = k"
proof -
  from p have "p 0 = 0" by (auto elim!: partitionsE)
  have "sum (λi. p (i + 1)) {..m - k} = sum (λi. p (i + 1)) {..m}"
    using partitions_decrease1[OF assms]
    by (auto intro: sum.mono_neutral_left elim!: partitionsE)
  also have "… = sum (λi. p (i + 1)) {0..m}" by (simp add: atLeast0AtMost)
  also have "… = sum (λi. p i) {Suc 0.. Suc m}"
    by (simp only: One_nat_def add_Suc_right add_0_right sum.shift_bounds_cl_Suc_ivl)
  also have "… = sum (λi. p i) {.. Suc m}"
    using ‹p 0 = 0› by (simp add: atLeast0AtMost sum_shift_lb_Suc0_0)
  also have "… = sum (λi. p i) {.. m}"
    using p by (auto elim!: partitionsE)
  also have "… = k"
    using sum by simp
  finally show ?thesis .
qed

lemma count_increase1:
  assumes partitions: "p partitions m - k"
  assumes k: "sum p {..m - k} = k"
  shows "(∑i≤m. p (i - 1)) = k"
proof -
  have "p 0 = 0" using partitions by (auto elim!: partitionsE)
  have "(∑i≤m. p (i - 1)) = (∑i∈{1..m}. p (i - 1))"
    using ‹p 0 = 0› by (auto intro: sum.mono_neutral_cong_right)
  also have "(∑i∈{1..m}. p (i - 1)) = (∑i≤m - 1. p i)"
  proof (cases m)
    case 0
    from this show ?thesis using ‹p 0 = 0› by simp
  next
    case (Suc m')
    {
      fix x assume "Suc 0 ≤ x" "x ≤ m"
      from this Suc have "x ∈ Suc ` {..m'}"
        by (auto intro!: image_eqI[where x="x - 1"])
    }
    from this Suc show ?thesis
      by (intro sum.reindex_cong[of Suc]) auto
  qed
  also have "(∑i≤m - 1. p i) = (∑i≤m. p i)"
  proof -
    {
      fix i
      assume "0 < p i" "i ≤ m"
      from assms this have "i ≤ m - 1"
        using ‹p 0 = 0› partitions_increase1 by (cases k) (auto elim!: partitionsE)
    }
    from this show ?thesis
      by (auto intro: sum.mono_neutral_cong_left)
  qed
  also have "... = (∑i≤m - k. p i)"
    using partitions by (auto intro: sum.mono_neutral_right elim!: partitionsE)
  also have "... = k" using k by auto
  finally show ?thesis .
qed

subsection ‹Number Partitions as Multisets on Natural Numbers›

definition number_partition :: "nat ⇒ nat multiset ⇒ bool"
where
  "number_partition n N = (sum_mset N = n ∧ 0 ∉# N)"

subsubsection ‹Relationship to Definition on Functions›

lemma count_partitions_iff:
  "count N partitions n ⟷ number_partition n N"
proof
  assume "count N partitions n"
  from this have "(∀i. count N i ≠ 0 ⟶ 1 ≤ i ∧ i ≤ n)" "(∑i≤n. count N i * i) = n"
    unfolding Number_Partition.partitions_def by auto
  moreover from this have "set_mset N ⊆ {..n}" by auto
  moreover have "finite {..n}" by auto
  ultimately have "sum_mset N = n"
    using sum_mset_sum_count sum_mset_eq_sum_on_supersets by presburger
  moreover have "0 ∉# N"
    using ‹∀i. count N i ≠ 0 ⟶ 1 ≤ i ∧ i ≤ n› by auto
  ultimately show "number_partition n N"
    unfolding number_partition_def by auto
next
  assume "number_partition n N"
  from this have "sum_mset N = n" and "0 ∉# N"
    unfolding number_partition_def by auto
  {
    fix i
    assume "count N i ≠ 0"
    have "1 ≤ i ∧ i ≤ n"
    proof
      from ‹0 ∉# N› ‹count N i ≠ 0› show "1 ≤ i"
        using Suc_le_eq by auto
      from ‹sum_mset N = n› ‹count N i ≠ 0› show "i ≤ n"
        using multi_member_split by fastforce
    qed
  }
  moreover from ‹sum_mset N = n› have "(∑i≤n. count N i * i) = n"
    by (metis atMost_iff calculation finite_atMost not_in_iff subsetI sum_mset_eq_sum_on_supersets sum_mset_sum_count)
  ultimately show "count N partitions n"
    by (rule partitionsI) auto
qed

lemma partitions_iff_Abs_multiset:
  "p partitions n ⟷ finite {x. 0 < p x} ∧ number_partition n (Abs_multiset p)"
proof
  assume "p partitions n"
  from this have bounds: "(∀i. p i ≠ 0 ⟶ 1 ≤ i ∧ i ≤ n)"
    and sum: "(∑i≤n. p i * i) = n"
  unfolding partitions_def by auto
  from ‹p partitions n› have "finite {x. 0 < p x}"
    by (rule partitions_imp_finite_elements)
  moreover from ‹finite {x. 0 < p x}› bounds have "¬ 0 ∈# Abs_multiset p"
    using count_eq_zero_iff by force
  moreover from ‹finite {x. 0 < p x}› this sum have "sum_mset (Abs_multiset p) = n"
  proof -
    have "(∑i∈{x. 0 < p x}. p i * i) = (∑i≤n. p i * i)"
      using bounds by (auto intro: sum.mono_neutral_cong_left)
    from ‹finite {x. 0 < p x}› this sum show "sum_mset (Abs_multiset p) = n"
      by (simp add: sum_mset_sum_count set_mset_Abs_multiset)
  qed
  ultimately show "finite {x. 0 < p x} ∧ number_partition n (Abs_multiset p)"
    unfolding number_partition_def by auto
next
  assume "finite {x. 0 < p x} ∧ number_partition n (Abs_multiset p)"
  from this have "finite {x. 0 < p x}" "0 ∉# Abs_multiset p" "sum_mset (Abs_multiset p) = n"
    unfolding number_partition_def by auto
  from ‹finite {x. 0 < p x}› have "(∑i∈{x. 0 < p x}. p i * i) = n"
    using ‹ sum_mset (Abs_multiset p) = n›
    by (simp add: sum_mset_sum_count set_mset_Abs_multiset)
  have bounds: "⋀i. p i ≠ 0 ⟹ 1 ≤ i ∧ i ≤ n"
  proof
    fix i
    assume "p i ≠ 0"
    from ‹¬ 0 ∈# Abs_multiset p› ‹finite {x. 0 < p x}› have "p 0 = 0"
      using count_inI by force
    from this ‹p i ≠ 0› show "1 ≤ i"
      by (metis One_nat_def leI less_Suc0)
    show "i ≤ n"
    proof (rule ccontr)
      assume "¬ i ≤ n"
      from this have "i > n"
        using le_less_linear by blast
      from this ‹p i ≠ 0› have "p i * i > n"
        by (auto simp add: less_le_trans)
      from ‹p i ≠ 0› have "(∑i∈{x. 0 < p x}. p i * i) = p i * i + (∑i∈{x. 0 < p x} - {i}. p i * i)"
        using ‹finite {x. 0 < p x}›
        by (subst sum.insert_remove[symmetric]) (auto simp add: insert_absorb)
      also from ‹p i * i > n› have "… > n" by auto
      finally show False using ‹(∑i∈{x. 0 < p x}. p i * i) = n› by blast
    qed
  qed
  moreover have "(∑i≤n. p i * i) = n"
  proof -
    have "(∑i≤n. p i * i) = (∑i∈{x. 0 < p x}. p i * i)"
      using bounds by (auto intro: sum.mono_neutral_cong_right)
    from this show ?thesis
      using ‹(∑i∈{x. 0 < p x}. p i * i) = n› by simp
  qed
  ultimately show "p partitions n" by (auto intro: partitionsI)
qed


lemma size_nat_multiset_eq:
  fixes N :: "nat multiset"
  assumes "number_partition n N"
  shows "size N = sum (count N) {..n}"
proof -
  have "set_mset N ⊆ {..sum_mset N}"
    by (auto dest: multi_member_split)
  have "size N = sum (count N) (set_mset N)"
    by (rule size_multiset_overloaded_eq)
  also have "… = sum (count N) {..sum_mset N}"
    using ‹set_mset N ⊆ {..sum_mset N}›
    by (auto intro: sum.mono_neutral_cong_left count_inI)
  finally show ?thesis
    using ‹number_partition n N›
    unfolding number_partition_def by auto
qed

end