law pow_succ_sym

bend-mathlib@0.8.1.0 · nat.bend:4196

import Base

4196# A power with a successor exponent: a^(n+1) = a * a^n, reversed to rewrite toward the simple side.
4197law pow_succ_sym:
4198  for -a: Nat
4199  for -n: Nat
4200  {Nat.mul(a, Nat.pow(a, n)) == Nat.pow(a, 1n+n) : Nat}