pub proof fn page_size_monotonic(a: PagingLevel, b: PagingLevel)Expand description
requires
1 <= a <= b <= NR_LEVELS + 1,page_size(a) <= page_size(b),page_size is monotonically increasing in its argument.