law two_pow_succ_sym

bend-mathlib@0.8.1.0 · nat.bend:4900

import Base

4900# Two to a successor power is double the power: 2^(n+1) = double (2^n), reversed to rewrite toward the simple side.
4901law two_pow_succ_sym:
4902  for n: Nat
4903  {Nat.double(Nat.pow(2n, n)) == Nat.pow(2n, 1n+n) : Nat}