law mod_mod_pow

lawful-words@0.1.0.0 · proof_nat.bend:1455

import Base

1455# (a % 2^m) % 2^k = a % 2^k for k <= m.
1456law mod_mod_pow:
1457  for +a: Nat
1458  for +k: Nat
1459  for +m: Nat
1460  for +h: {Nat.is_le(k, m) == True{} : Bool}
1461  {Nat.mod(Nat.mod(a, Nat.pow(2n, m)), Nat.pow(2n, k)) == Nat.mod(a, Nat.pow(2n, k)) : Nat}