pub proof fn lemma_nr_subpage_per_huge_bounded<C: PagingConstsTrait>()Expand description
ensures
0 < nr_subpage_per_huge::<C>() <= C::BASE_PAGE_SIZE(),pub proof fn lemma_nr_subpage_per_huge_bounded<C: PagingConstsTrait>()0 < nr_subpage_per_huge::<C>() <= C::BASE_PAGE_SIZE(),