law one_pow_sym

bend-mathlib@0.8.1.0 · nat.bend:4213

import Base

4213# One to any power is one, reversed to rewrite toward the simple side.
4214law one_pow_sym:
4215  for n: Nat
4216  {1n == Nat.pow(1n, n) : Nat}