∀ {α : Type u_1} [inst : Semiring α] {f : α → ℕ → α} {a : α} {a' b b' c n n' : ℕ},
  CharP α n →
    f = HPow.hPow →
      Mathlib.Meta.NormNum.IsNat a a' →
        Mathlib.Meta.NormNum.IsNat b b' →
          Mathlib.Meta.NormNum.IsNat n n' → (a'.pow b').mod n' = c → Mathlib.Meta.NormNum.IsNat (f a b) c