law pow_sub1

lawful-words@0.1.0.0 · proof_nat.bend:1409

import Base

1409# 2^(1+j) - 1 = 1 + 2 (2^j - 1).
1410law pow_sub1:
1411  for +j: Nat
1412  {Nat.sub(Nat.pow(2n, 1n+j), 1n) == 1n+Nat.double(Nat.sub(Nat.pow(2n, j), 1n)) : Nat}