law one_pow

bend-mathlib@0.8.1.0 · nat.bend:1219

import Base

1219# One to any power is one.
1220law one_pow:
1221  for n: Nat
1222  {Nat.pow(1n, n) == 1n : Nat}