law pow_zero_sym

bend-mathlib@0.8.1.0 · nat.bend:4188

import Base

4188# Any natural to the power zero is one, reversed to rewrite toward the simple side.
4189law pow_zero_sym:
4190  for -a: Nat
4191  {1n == Nat.pow(a, 0n) : Nat}