law pow_one

bend-mathlib@0.8.1.0 · nat.bend:1211

import Base

1211# Any natural to the power one is itself.
1212law pow_one:
1213  for a: Nat
1214  {Nat.pow(a, 1n) == a : Nat}