law exk

lawful-bytes@0.1.1.0 · proof_fast_append.bend:1069

import Base

1069law exk:
1070  for +ld: U32
1071  for +k: Nat
1072  for +ek: {U32.to_nat((ld .&. 3 : U32)) == k : Nat}
1073  {U32.to_nat(ld) == Nat.add(Nat.mul(Nat.div(U32.to_nat(ld), 4n), 4n), k) : Nat}