~/jendhub

law from_nat_mul.m

lawful-words@0.1.0.0 · proof_u32.bend:468

import lawful-words@0.1.0.0/proof_u32.bend as ProofU32
import Base

468law from_nat_mul.m:
469  for +x: Nat
470  for +y: Nat
471  for +m: Nat
472  for +hm: {Nat.pow(2n, 32n) == m : Nat}
473  {U32.from_nat(Nat.mul(x, y)) == U32.mul(U32.from_nat(x), U32.from_nat(y)) : U32}

Uses (14)

Used by (1)