law p16

lawful-words@0.1.0.0 · proof_bytes.bend:1430

import Base

1430# 2^16, 2^24 and 2^32 in terms of a = 2^8.
1431law p16:
1432  for +a: Nat
1433  for +ha: {Nat.pow(2n, 8n) == a : Nat}
1434  {Nat.pow(2n, 16n) == Nat.mul(a, a) : Nat}