∀ (K : Type u_1) [inst : CommRing K] (p : ℕ) [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP K p] (n : ℕ) (x : K),
  ((n, x).1 + (0, 1).1, (⇑(frobenius K p))^[(0, 1).1] (n, x).2 * (⇑(frobenius K p))^[(n, x).1] (0, 1).2) = (n, x)