pub proof fn lemma_count_present_upto_present<E: PageTableEntryTrait>(
s: Seq<E>,
n: int,
idx: int,
)Expand description
requires
0 <= idx < n,s[idx].is_present(),count_present_upto(s, n) >= 1,A present slot below n makes the count at least 1.