law n_half

lawful-arrays@0.1.0.0 · proof_index.bend:17

import Base

17law n_half:
18  for +p: Nat
19  {Nat.div(Nat.pow(2n, 1n+p), 2n) == Nat.pow(2n, p) : Nat}