law pow2s

lawful-words@0.1.0.0 · proof_nat.bend:1402

import Base

1402law pow2s:
1403  for +p: Nat
1404  {Nat.pow(2n, 1n+p) == Nat.double(Nat.pow(2n, p)) : Nat}