law pow_succ

bend-mathlib@0.8.1.0 · nat.bend:1202

import Base

1202# A power with a successor exponent: a^(n+1) = a * a^n.
1203law pow_succ:
1204  for -a: Nat
1205  for -n: Nat
1206  {Nat.pow(a, 1n+n) == Nat.mul(a, Nat.pow(a, n)) : Nat}