Function lemma_aligned_indices_zero 

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

requires

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

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

ensures

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

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

Slot alignment makes every lower PTE index zero.