pub broadcast proof fn lemma_usize_low_bits_mask_is_mod(x: usize, n: nat)Expand description
requires
n < <usize>::BITS,#[trigger] (x & (low_bits_mask(n) as usize)) == x % (pow2(n) as usize),Proof that for natural n and x of type usize , and with the low n-bit mask is equivalent to modulo 2^n.