law pow_zero

bend-mathlib@0.8.1.0 · nat.bend:1194

import Base

1194# Any natural to the power zero is one.
1195law pow_zero:
1196  for -a: Nat
1197  {Nat.pow(a, 0n) == 1n : Nat}