pub proof fn lemma_count_present_upto_bound<E: PageTableEntryTrait>(s: Seq<E>, n: int)Expand description
requires
0 <= n,0 <= count_present_upto(s, n) <= n,count_present_upto is between 0 and n.