law two_pow_succ

bend-mathlib@0.8.1.0 · nat.bend:3821

import Base

3821# Two to a successor power is double the power: 2^(n+1) = double (2^n).
3822law two_pow_succ:
3823  for n: Nat
3824  {Nat.pow(2n, 1n+n) == Nat.double(Nat.pow(2n, n)) : Nat}