law shq2

lawful-bytes@0.1.1.0 · proof_fast_append.bend:481

import Base

481law shq2:
482  for +x: U32
483  for +r: Nat
484  for +e: {U32.to_nat(x) == r : Nat}
485  for +hr: {Nat.is_lt(r, 4n) == True{} : Bool}
486  {U32.to_nat((x << 3n : U32)) == Nat.mul(8n, U32.to_nat(x)) : Nat}