law nat_mod_mod_pow

lawful-words@0.1.0.0 · LAWS.bend:583

import Base

583# (a % 2^m) % 2^k = a % 2^k for k <= m.
584law nat_mod_mod_pow:
585  for a: Nat
586  for k: Nat
587  for m: Nat
588  for h: {Nat.is_le(k, m) == True{} : Bool}
589  {Nat.mod(Nat.mod(a, Nat.pow(2n, m)), Nat.pow(2n, k)) == Nat.mod(a, Nat.pow(2n, k)) : Nat}