Theory Partial_Order_Reduction.ESet_Extensions

section ‹Sets and Extended Natural Numbers›

theory ESet_Extensions
imports
  "../Basics/Functions"
  Basic_Extensions
  CCPO_Extensions
begin

  lemma card_lessThan_enat[simp]: "card {..< enat k} = card {..< k}"
  proof -
    have 1: "{..< enat k} = enat ` {..< k}"
      unfolding lessThan_def image_Collect using enat_iless by force
    have "card {..< enat k} = card (enat ` {..< k})" unfolding 1 by rule
    also have "… = card {..< k}" using card_image inj_enat by metis
    finally show ?thesis by this
  qed
  lemma card_atMost_enat[simp]: "card {.. enat k} = card {.. k}"
  proof -
    have 1: "{.. enat k} = enat ` {.. k}"
      unfolding atMost_def image_Collect using enat_ile by force
    have "card {.. enat k} = card (enat ` {.. k})" unfolding 1 by rule
    also have "… = card {.. k}" using card_image inj_enat by metis
    finally show ?thesis by this
  qed

  lemma enat_Collect:
    assumes "∞ ∉ A"
    shows "{i. enat i ∈ A} = the_enat ` A"
    using assms by (safe, force) (metis enat_the_enat)

  lemma Collect_lessThan: "{i. enat i < n} = the_enat ` {..< n}"
  proof -
    have 1: "∞ ∉ {..< n}" by simp
    have "{i. enat i < n} = {i. enat i ∈ {..< n}}" by simp
    also have "… = the_enat ` {..< n}" using enat_Collect 1 by this
    finally show ?thesis by this
  qed

  instantiation set :: (type) esize_ccpo
  begin

    function esize_set where "finite A ⟹ esize A = enat (card A)" | "infinite A ⟹ esize A = ∞"
      by auto termination by lexicographic_order

    lemma esize_iff_empty[iff]: "esize A = 0 ⟷ A = {}" by (cases "finite A", auto)
    lemma esize_iff_infinite[iff]: "esize A = ∞ ⟷ infinite A" by force
    lemma esize_singleton[simp]: "esize {a} = eSuc 0" by simp
    lemma esize_infinite_enat[dest, simp]: "infinite A ⟹ enat k < esize A" by force

    instance
    proof
      fix A :: "'a set"
      assume 1: "esize A ≠ ∞"
      show "finite {B. B ⊆ A}" using 1 by simp
    next
      fix A B :: "'a set"
      assume 1: "A ⊆ B"
      show "esize A ≤ esize B"
      proof (cases "finite B")
        case False
        show ?thesis using False by auto
      next
        case True
        have 2: "finite A" using True 1 by auto
        show ?thesis using card_mono True 1 2 by auto
      qed
    next
      fix A B :: "'a set"
      assume 1: "esize A ≠ ∞" "A ⊂ B"
      show "esize A < esize B" using psubset_card_mono 1 by (cases "finite B", auto)
    qed

  end

  lemma esize_image[simp, intro]:
    assumes "inj_on f A"
    shows "esize (f ` A) = esize A"
    using card_image finite_imageD assms by (cases "finite A", auto)
  lemma esize_insert1[simp]: "a ∉ A ⟹ esize (insert a A) = eSuc (esize A)"
    by (cases "finite A", force+)
  lemma esize_insert2[simp]: "a ∈ A ⟹ esize (insert a A) = esize A"
    using insert_absorb by metis
  lemma esize_remove1[simp]: "a ∉ A ⟹ esize (A - {a}) = esize A"
    by (cases "finite A", force+)
  lemma esize_remove2[simp]: "a ∈ A ⟹ esize (A - {a}) = epred (esize A)"
    by (cases "finite A", force+)
  lemma esize_union_disjoint[simp]:
    assumes "A ∩ B = {}"
    shows "esize (A ∪ B) = esize A + esize B"
  proof (cases "finite (A ∪ B)")
    case True
    show ?thesis using card_Un_disjoint assms True by auto
  next
    case False
    show ?thesis using False by (cases "finite A", auto)
  qed
  lemma esize_lessThan[simp]: "esize {..< n} = n"
  proof (cases n)
    case (enat k)
    have 1: "finite {..< n}" unfolding enat by (metis finite_lessThan_enat_iff not_enat_eq)
    show ?thesis using 1 unfolding enat by simp
  next
    case (infinity)
    have 1: "infinite {..< n}" unfolding infinity using infinite_lessThan_infty by simp
    show ?thesis using 1 unfolding infinity by simp
  qed
  lemma esize_atMost[simp]: "esize {.. n} = eSuc n"
  proof (cases n)
    case (enat k)
    have 1: "finite {.. n}" unfolding enat by (metis atMost_iff finite_enat_bounded)
    show ?thesis using 1 unfolding enat by simp
  next
    case (infinity)
    have 1: "infinite {.. n}"
      unfolding infinity
      by (metis atMost_iff enat_ord_code(3) infinite_lessThan_infty infinite_super subsetI)
    show ?thesis using 1 unfolding infinity by simp
  qed

  lemma least_eSuc[simp]:
    assumes "A ≠ {}"
    shows "least (eSuc ` A) = eSuc (least A)"
  proof (rule antisym)
    obtain k where 10: "k ∈ A" using assms by blast
    have 11: "eSuc k ∈ eSuc ` A" using 10 by auto
    have 20: "least A ∈ A" using 10 LeastI by metis
    have 21: "least (eSuc ` A) ∈ eSuc ` A" using 11 LeastI by metis
    have 30: "⋀ l. l ∈ A ⟹ least A ≤ l" using 10 Least_le by metis
    have 31: "⋀ l. l ∈ eSuc ` A ⟹ least (eSuc ` A) ≤ l" using 11 Least_le by metis
    show "least (eSuc ` A) ≤ eSuc (least A)" using 20 31 by auto
    show "eSuc (least A) ≤ least (eSuc ` A)" using 21 30 by auto
  qed

  lemma Inf_enat_eSuc[simp]: "⨅ (eSuc ` A) = eSuc (⨅ A)" unfolding Inf_enat_def by simp

  definition lift :: "nat set ⇒ nat set"
    where "lift A ≡ insert 0 (Suc ` A)"

  lemma liftI_0[intro, simp]: "0 ∈ lift A" unfolding lift_def by auto
  lemma liftI_Suc[intro]: "a ∈ A ⟹ Suc a ∈ lift A" unfolding lift_def by auto
  lemma liftE[elim]:
    assumes "b ∈ lift A"
    obtains (0) "b = 0" | (Suc) a where "b = Suc a" "a ∈ A"
    using assms unfolding lift_def by auto

  lemma lift_esize[simp]: "esize (lift A) = eSuc (esize A)" unfolding lift_def by auto  
  lemma lift_least[simp]: "least (lift A) = 0" unfolding lift_def by auto

  primrec nth_least :: "'a set ⇒ nat ⇒ 'a :: wellorder"
    where "nth_least A 0 = least A" | "nth_least A (Suc n) = nth_least (A - {least A}) n"

  lemma nth_least_wellformed[intro?, simp]:
    assumes "enat n < esize A"
    shows "nth_least A n ∈ A"
  using assms
  proof (induct n arbitrary: A)
    case 0
    show ?case using 0 by simp
  next
    case (Suc n)
    have 1: "A ≠ {}" using Suc(2) by auto
    have 2: "enat n < esize (A - {least A})" using Suc(2) 1 by simp
    have 3: "nth_least (A - {least A}) n ∈ A - {least A}" using Suc(1) 2 by this
    show ?case using 3 by simp
  qed

  lemma card_wellformed[intro?, simp]:
    fixes k :: "'a :: wellorder"
    assumes "k ∈ A"
    shows "enat (card {i ∈ A. i < k}) < esize A"
  proof (cases "finite A")
    case False
    show ?thesis using False by simp
  next
    case True
    have 1: "esize {i ∈ A. i < k} < esize A" using True assms by fastforce
    show ?thesis using True 1 by simp
  qed

  lemma nth_least_strict_mono:
    assumes "enat l < esize A" "k < l"
    shows "nth_least A k < nth_least A l"
  using assms
  proof (induct k arbitrary: A l)
    case 0
    obtain l' where 1: "l = Suc l'" using 0(2) by (metis gr0_conv_Suc)
    have 2: "A ≠ {}" using 0(1) by auto
    have 3: "enat l' < esize (A - {least A})" using 0(1) 2 unfolding 1 by simp
    have 4: "nth_least (A - {least A}) l' ∈ A - {least A}" using 3 by rule
    show ?case using 1 4 by (auto intro: le_neq_trans)
  next
    case (Suc k)
    obtain l' where 1: "l = Suc l'" using Suc(3) by (metis Suc_lessE)
    have 2: "A ≠ {}" using Suc(2) by auto
    show ?case using Suc 2 unfolding 1 by simp
  qed
    
  lemma nth_least_mono[intro, simp]:
    assumes "enat l < esize A" "k ≤ l"
    shows "nth_least A k ≤ nth_least A l"
    using nth_least_strict_mono le_less assms by metis

  lemma card_nth_least[simp]:
    assumes "enat n < esize A"
    shows "card {k ∈ A. k < nth_least A n} = n"
  using assms
  proof (induct n arbitrary: A)
    case 0
    have 1: "{k ∈ A. k < least A} = {}" using least_not_less by auto
    show ?case using nth_least.simps(1) card.empty 1 by metis
  next
    case (Suc n)
    have 1: "A ≠ {}" using Suc(2) by auto
    have 2: "enat n < esize (A - {least A})" using Suc(2) 1 by simp
    have 3: "nth_least A 0 < nth_least A (Suc n)" using nth_least_strict_mono Suc(2) by blast
    have 4: "{k ∈ A. k < nth_least A (Suc n)} =
      {least A} ∪ {k ∈ A - {least A}. k < nth_least (A - {least A}) n}" using 1 3 by auto
    have 5: "card {k ∈ A - {least A}. k < nth_least (A - {least A}) n} = n" using Suc(1) 2 by this
    have 6: "finite {k ∈ A - {least A}. k < nth_least (A - {least A}) n}"
      using 5 Collect_empty_eq card.infinite infinite_imp_nonempty least_not_less nth_least.simps(1)
      by (metis (no_types, lifting))
    have "card {k ∈ A. k < nth_least A (Suc n)} =
      card ({least A} ∪ {k ∈ A - {least A}. k < nth_least (A - {least A}) n})" using 4 by simp
    also have "… = card {least A} + card {k ∈ A - {least A}. k < nth_least (A - {least A}) n}"
      using 6 by simp
    also have "… = Suc n" using 5 by simp
    finally show ?case by this
  qed

  lemma card_nth_least_le[simp]:
    assumes "enat n < esize A"
    shows "card {k ∈ A. k ≤ nth_least A n} = Suc n"
  proof -
    have 1: "{k ∈ A. k ≤ nth_least A n} = {nth_least A n} ∪ {k ∈ A. k < nth_least A n}"
      using assms by auto
    have 2: "card {k ∈ A. k < nth_least A n} = n" using assms by simp
    have 3: "finite {k ∈ A. k < nth_least A n}"
      using 2 Collect_empty_eq card.infinite infinite_imp_nonempty least_not_less nth_least.simps(1)
      by (metis (no_types, lifting))
    have "card {k ∈ A. k ≤ nth_least A n} = card ({nth_least A n} ∪ {k ∈ A. k < nth_least A n})"
      unfolding 1 by rule
    also have "… = card {nth_least A n} + card {k ∈ A. k < nth_least A n}" using 3 by simp
    also have "… = Suc n" using assms by simp
    finally show ?thesis by this
  qed

  lemma nth_least_card:
    fixes k :: nat
    assumes "k ∈ A"
    shows "nth_least A (card {i ∈ A. i < k}) = k"
  proof (rule nat_set_card_equality_less)
    have 1: "enat (card {l ∈ A. l < k}) < esize A"
    proof (cases "finite A")
      case False
      show ?thesis using False by simp
    next
      case True
      have 1: "{l ∈ A. l < k} ⊂ A" using assms by blast
      have 2: "card {l ∈ A. l < k} < card A" using psubset_card_mono True 1 by this
      show ?thesis using True 2 by simp
    qed
    show "nth_least A (card {l ∈ A. l < k}) ∈ A" using 1 by rule
    show "k ∈ A" using assms by this
    show "card {z ∈ A. z < nth_least A (card {i ∈ A. i < k})} = card {z ∈ A. z < k}" using 1 by simp
  qed

  interpretation nth_least:
    bounded_function_pair "{i. enat i < esize A}" "A" "nth_least A" "λ k. card {i ∈ A. i < k}"
    using nth_least_wellformed card_wellformed by (unfold_locales, blast+)

  interpretation nth_least:
    injection "{i. enat i < esize A}" "A" "nth_least A" "λ k. card {i ∈ A. i < k}"
    using card_nth_least by (unfold_locales, blast)

  interpretation nth_least:
    surjection "{i. enat i < esize A}" "A" "nth_least A" "λ k. card {i ∈ A. i < k}"
    for A :: "nat set"
    using nth_least_card by (unfold_locales, blast)

  interpretation nth_least:
    bijection "{i. enat i < esize A}" "A" "nth_least A" "λ k. card {i ∈ A. i < k}"
    for A :: "nat set"
    by unfold_locales

  lemma nth_least_strict_mono_inverse:
    fixes A :: "nat set"
    assumes "enat k < esize A" "enat l < esize A" "nth_least A k < nth_least A l"
    shows "k < l"
    using assms by (metis not_less_iff_gr_or_eq nth_least_strict_mono)

  lemma nth_least_less_card_less:
    fixes k :: nat
    shows "enat n < esize A ∧ nth_least A n < k ⟷ n < card {i ∈ A. i < k}"
  proof safe
    assume 1: "enat n < esize A" "nth_least A n < k"
    have 2: "nth_least A n ∈ A" using 1(1) by rule
    have "n = card {i ∈ A. i < nth_least A n}" using 1 by simp
    also have "… < card {i ∈ A. i < k}" using 1(2) 2 by simp
    finally show "n < card {i ∈ A. i < k}" by this
  next
    assume 1: "n < card {i ∈ A. i < k}"
    have "enat n < enat (card {i ∈ A. i < k})" using 1 by simp
    also have "… = esize {i ∈ A. i < k}" by simp
    also have "… ≤ esize A" by blast
    finally show 2: "enat n < esize A" by this
    have 3: "n = card {i ∈ A. i < nth_least A n}" using 2 by simp
    have 4: "card {i ∈ A. i < nth_least A n} < card {i ∈ A. i < k}" using 1 2 by simp
    have 5: "nth_least A n ∈ A" using 2 by rule
    show "nth_least A n < k" using 4 5 by simp
  qed

  lemma nth_least_less_esize_less:
    "enat n < esize A ∧ enat (nth_least A n) < k ⟷ enat n < esize {i ∈ A. enat i < k}"
    using nth_least_less_card_less by (cases k, simp+)

  lemma nth_least_le:
    assumes "enat n < esize A"
    shows "n ≤ nth_least A n"
  using assms
  proof (induct n)
    case 0
    show ?case using 0 by simp
  next
    case (Suc n)
    have "n ≤ nth_least A n" using Suc by (metis Suc_ile_eq less_imp_le)
    also have "… < nth_least A (Suc n)" using nth_least_strict_mono Suc(2) by blast
    finally show ?case by simp
  qed

  lemma nth_least_eq:
    assumes "enat n < esize A" "enat n < esize B"
    assumes "⋀ i. i ≤ nth_least A n ⟹ i ≤ nth_least B n ⟹ i ∈ A ⟷ i ∈ B"
    shows "nth_least A n = nth_least B n"
  using assms
  proof (induct n arbitrary: A B)
    case 0
    have 1: "least A = least B"
    proof (rule least_eq)
      show "A ≠ {}" using 0(1) by simp
      show "B ≠ {}" using 0(2) by simp
    next
      fix i
      assume 2: "i ≤ least A" "i ≤ least B"
      show "i ∈ A ⟷ i ∈ B" using 0(3) 2 unfolding nth_least.simps by this
    qed
    show ?case using 1 by simp
  next
    case (Suc n)
    have 1: "A ≠ {}" "B ≠ {}" using Suc(2, 3) by auto
    have 2: "least A = least B"
    proof (rule least_eq)
      show "A ≠ {}" using 1(1) by this
      show "B ≠ {}" using 1(2) by this
    next
      fix i
      assume 3: "i ≤ least A" "i ≤ least B"
      have 4: "nth_least A 0 ≤ nth_least A (Suc n)" using Suc(2) by blast
      have 5: "nth_least B 0 ≤ nth_least B (Suc n)" using Suc(3) by blast
      have 6: "i ≤ nth_least A (Suc n)" "i ≤ nth_least B (Suc n)" using 3 4 5 by auto
      show "i ∈ A ⟷ i ∈ B" using Suc(4) 6 by this
    qed
    have 3: "nth_least (A - {least A}) n = nth_least (B - {least B}) n"
    proof (rule Suc(1))
      show "enat n < esize (A - {least A})" using Suc(2) 1(1) by simp
      show "enat n < esize (B - {least B})" using Suc(3) 1(2) by simp
    next
      fix i
      assume 3: "i ≤ nth_least (A - {least A}) n" "i ≤ nth_least (B - {least B}) n"
      have 4: "i ≤ nth_least A (Suc n)" "i ≤ nth_least B (Suc n)" using 3 by simp+
      have 5: "i ∈ A ⟷ i ∈ B" using Suc(4) 4 by this
      show "i ∈ A - {least A} ⟷ i ∈ B - {least B}" using 2 5 by auto
    qed
    show ?case using 3 by simp
  qed

  lemma nth_least_restrict[simp]:
    assumes "enat i < esize {i ∈ s. enat i < k}"
    shows "nth_least {i ∈ s. enat i < k} i = nth_least s i"
  proof (rule nth_least_eq)
    show "enat i < esize {i ∈ s. enat i < k}" using assms by this
    show "enat i < esize s" using nth_least_less_esize_less assms by auto
  next
    fix l
    assume 1: "l ≤ nth_least {i ∈ s. enat i < k} i"
    have 2: "nth_least {i ∈ s. enat i < k} i ∈ {i ∈ s. enat i < k}" using assms by rule
    have "enat l ≤ enat (nth_least {i ∈ s. enat i < k} i)" using 1 by simp
    also have "… < k" using 2 by simp
    finally show "l ∈ {i ∈ s. enat i < k} ⟷ l ∈ s" by auto
  qed

  lemma least_nth_least[simp]:
    assumes "A ≠ {}" "⋀ i. i ∈ A ⟹ enat i < esize B"
    shows "least (nth_least B ` A) = nth_least B (least A)"
    using assms by simp

  lemma nth_least_nth_least[simp]:
    assumes "enat n < esize A" "⋀ i. i ∈ A ⟹ enat i < esize B"
    shows "nth_least B (nth_least A n) = nth_least (nth_least B ` A) n"
  using assms
  proof (induct n arbitrary: A)
    case 0
    show ?case using 0 by simp
  next
    case (Suc n)
    have 1: "A ≠ {}" using Suc(2) by auto
    have 2: "nth_least B ` (A - {least A}) = nth_least B ` A - nth_least B ` {least A}"
    proof (rule inj_on_image_set_diff)
      show "inj_on (nth_least B) {i. enat i < esize B}" using nth_least.inj_on by this
      show "A - {least A} ⊆ {i. enat i < esize B}" using Suc(3) by blast
      show "{least A} ⊆ {i. enat i < esize B}" using Suc(3) 1 by force
    qed
    have "nth_least B (nth_least A (Suc n)) = nth_least B (nth_least (A - {least A}) n)" by simp
    also have "… = nth_least (nth_least B ` (A - {least A})) n" using Suc 1 by force
    also have "… = nth_least (nth_least B ` A - nth_least B ` {least A}) n" unfolding 2 by rule
    also have "… = nth_least (nth_least B ` A - {nth_least B (least A)}) n" by simp
    also have "… = nth_least (nth_least B ` A - {least (nth_least B ` A)}) n" using Suc(3) 1 by auto
    also have "… = nth_least (nth_least B ` A) (Suc n)" by simp
    finally show ?case by this
  qed

  lemma nth_least_Max[simp]:
    assumes "finite A" "A ≠ {}"
    shows "nth_least A (card A - 1) = Max A"
  using assms
  proof (induct "card A - 1" arbitrary: A)
    case 0
    have 1: "card A = 1" using 0 by (metis One_nat_def Suc_diff_1 card_gt_0_iff)
    obtain a where 2: "A = {a}" using 1 by rule
    show ?case unfolding 2 by (simp del: insert_iff)
  next
    case (Suc n)
    have 1: "least A ∈ A" using Suc(4) by rule
    have 2: "card (A - {least A}) = Suc n" using Suc(2, 3) 1 by simp
    have 3: "A - {least A} ≠ {}" using 2 Suc(3) by fastforce
    have "nth_least A (card A - 1) = nth_least A (Suc n)" unfolding Suc(2) by rule
    also have "… = nth_least (A - {least A}) n" by simp
    also have "… = nth_least (A - {least A}) (card (A - {least A}) - 1)" unfolding 2 by simp
    also have "… = Max (A - {least A})"
    proof (rule Suc(1))
      show "n = card (A - {least A}) - 1" unfolding 2 by simp
      show "finite (A - {least A})" using Suc(3) by simp
      show "A - {least A} ≠ {}" using 3 by this
    qed
    also have "… = Max A" using Suc(3) 3 by simp
    finally show ?case by this
  qed

  lemma nth_least_le_Max:
    assumes "finite A" "A ≠ {}" "enat n < esize A"
    shows "nth_least A n ≤ Max A"
  proof -
    have "nth_least A n ≤ nth_least A (card A - 1)"
    proof (rule nth_least_mono)
      show "enat (card A - 1) < esize A" by (metis Suc_diff_1 Suc_ile_eq assms(1) assms(2)
        card_eq_0_iff esize_set.simps(1) not_gr0 order_refl)
      show "n ≤ card A - 1" by (metis Suc_diff_1 Suc_leI antisym_conv assms(1) assms(3)
        enat_ord_simps(2) esize_set.simps(1) le_less neq_iff not_gr0)
    qed
    also have "… = Max A" using nth_least_Max assms(1, 2) by this
    finally show ?thesis by this
  qed

  lemma nth_least_not_contains:
    fixes k :: nat
    assumes "enat (Suc n) < esize A" "nth_least A n < k" "k < nth_least A (Suc n)"
    shows "k ∉ A"
  proof
    assume 1: "k ∈ A"
    have 2: "nth_least A (card {i ∈ A. i < k}) = k" using nth_least.right_inverse 1 by this
    have 3: "n < card {i ∈ A. i < k}"
    proof (rule nth_least_strict_mono_inverse)
      show "enat n < esize A" using assms(1) by auto
      show "enat (card {i ∈ A. i < k}) < esize A" using nth_least.g.wellformed 1 by simp
      show "nth_least A n < nth_least A (card {i ∈ A. i < k})" using assms(2) 2 by simp
    qed
    have 4: "card {i ∈ A. i < k} < Suc n"
    proof (rule nth_least_strict_mono_inverse)
      show "enat (card {i ∈ A. i < k}) < esize A" using nth_least.g.wellformed 1 by simp
      show "enat (Suc n) < esize A" using assms(1) by this
      show "nth_least A (card {i ∈ A. i < k}) < nth_least A (Suc n)" using assms(3) 2 by simp
    qed
    show "False" using 3 4 by auto
  qed

  lemma nth_least_Suc[simp]:
    assumes "enat n < esize A"
    shows "nth_least (Suc ` A) n = Suc (nth_least A n)"
  using assms
  proof (induct n arbitrary: A)
    case (0)
    have 1: "A ≠ {}" using 0 by auto
    show ?case using 1 by simp
  next
    case (Suc n)
    have 1: "enat n < esize (A - {least A})"
    proof -
      have 2: "A ≠ {}" using Suc(2) by auto
      have 3: "least A ∈ A" using LeastI 2 by fast
      have 4: "A = insert (least A) A" using 3 by auto
      have "eSuc (enat n) = enat (Suc n)" by simp
      also have "… < esize A" using Suc(2) by this
      also have "… = esize (insert (least A) A)" using 4 by simp
      also have "… = eSuc (esize (A - {least A}))" using 3 2 by simp
      finally show ?thesis using Extended_Nat.eSuc_mono by metis
    qed
    have "nth_least (Suc ` A) (Suc n) = nth_least (Suc ` A - {least (Suc ` A)}) n" by simp
    also have "… = nth_least (Suc ` (A - {least A})) n" by simp
    also have "… = Suc (nth_least (A - {least A}) n)" using Suc(1) 1 by this
    also have "… = Suc (nth_least A (Suc n))" by simp
    finally show ?case by this
  qed

  lemma nth_least_lift[simp]:
    "nth_least (lift A) 0 = 0"
    "enat n < esize A ⟹ nth_least (lift A) (Suc n) = Suc (nth_least A n)"
    unfolding lift_def by simp+

  lemma nth_least_list_card[simp]:
    assumes "enat n ≤ esize A"
    shows "card {k ∈ A. k < nth_least (lift A) n} = n"
    using less_Suc_eq_le assms by (cases n, auto simp del: nth_least.simps)

end