[STATEMENT]
lemma nth_least_list_card[simp]:
    assumes "enat n \<le> esize A"
    shows "card {k \<in> A. k < nth_least (lift A) n} = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {k \<in> A. k < nth_least (lift A) n} = n
[PROOF STEP]
using less_Suc_eq_le assms
[PROOF STATE]
proof (prove)
using this:
(?m < Suc ?n) = (?m \<le> ?n)
enat n \<le> esize A

goal (1 subgoal):
 1. card {k \<in> A. k < nth_least (lift A) n} = n
[PROOF STEP]
by (cases n, auto simp del: nth_least.simps)