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