law mul4div

lawful-bytes@0.1.1.0 · proof_fast_append.bend:1039

import lawful-bytes@0.1.1.0/proof_fast_append.bend as ProofFastAppend

import Base

1039law mul4div:
1040  for +z: Nat
1041  for +y: Nat
1042  for +e: {z == Nat.mul(y, 4n) : Nat}
1043  {Nat.mul(Nat.div(z, 4n), 4n) == z : Nat}

Uses (9)

Used by (1)

lawful-bytes@0.1.1.0/proof_fast_append:align2