law pow_one_plus

lawful-words@0.1.0.0 · proof_nat.bend:1418

import Base

1418law pow_one_plus:
1419  for +k: Nat
1420  {1n+Nat.sub(Nat.pow(2n, k), 1n) == Nat.pow(2n, k) : Nat}