Expand description
Bounded-arithmetic proofs for vaddr_range’s body.
Factored into a leaf module because the nonlinear_arith tactic
triggers a Verus internal panic when used in page_table/mod.rs
alongside largest_pages (which has an impl Iterator return type).
Same workaround pattern as the older vaddr_range_bv_lemmas.