Function lemma_pte_index_spec_is_div_mod 

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

requires

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

ensures

pte_index_spec::<C>(va, level)
    == (va / page_size::<C>(level)) % nr_subpage_per_huge::<C>(),

Selecting an index is division by the slot size followed by reduction modulo the fanout.