Function lemma_lower_indices_aligned 

pub proof fn lemma_lower_indices_aligned<C: PagingConstsTrait>(
    va: Vaddr,
    level: PagingLevel,
)

requires

1 <= level <= C::NR_LEVELS() + 1,

va % C::BASE_PAGE_SIZE() == 0,

forall |i: int| {
    1 <= i < level ==> #[trigger] pte_index_spec::<C>(va, i as PagingLevel) == 0
},

ensures

va % page_size::<C>(level) == 0,

Zero lower indices together with base-page alignment imply slot alignment.