pub proof fn lemma_count_present_upto_absent<E: PageTableEntryTrait>(
s: Seq<E>,
n: int,
idx: int,
)Expand description
requires
0 <= idx < n,!s[idx].is_present(),count_present_upto(s, n) < n,An absent slot below n makes the count strictly less than n.