law zero_pow_sym

bend-mathlib@0.8.1.0 · nat.bend:4493

import Base

4493# Zero to a positive power is zero: 0^(n+1) = 0, reversed to rewrite toward the simple side.
4494law zero_pow_sym:
4495  for -n: Nat
4496  {0n == Nat.pow(0n, 1n+n) : Nat}