law p24

lawful-words@0.1.0.0 · proof_bytes.bend:1441

import Base

1441law p24:
1442  for +a: Nat
1443  for +ha: {Nat.pow(2n, 8n) == a : Nat}
1444  {Nat.pow(2n, 24n) == Nat.mul(Nat.mul(a, a), a) : Nat}