K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y1 y2 : ℕ × K
H : R K p y1 y2
n : ℕ
y : K
⊢ R K p (x.fst + (n, y).fst, (↑(frobenius K p)^[(n, y).fst]) x.snd + (↑(frobenius K p)^[x.fst]) (n, y).snd)
    (x.fst + (n + 1, ↑(frobenius K p) y).fst,
      ↑(frobenius K p) ((↑(frobenius K p)^[n]) x.snd + (↑(frobenius K p)^[x.fst]) y))
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y1 y2 : ℕ × K
H : R K p y1 y2
n : ℕ
y : K
⊢ R K p (x.fst + (n, y).fst, (↑(frobenius K p)^[(n, y).fst]) x.snd + (↑(frobenius K p)^[x.fst]) (n, y).snd)
    (x.fst + (n + 1, ↑(frobenius K p) y).fst,
      (↑(frobenius K p)^[(n + 1, ↑(frobenius K p) y).fst]) x.snd +
        (↑(frobenius K p)^[x.fst]) (n + 1, ↑(frobenius K p) y).snd)
rw [← iterate_succ_apply, iterate_succ_apply', iterate_succ_apply', ← frobenius_add]
no goals
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y1 y2 : ℕ × K
H : R K p y1 y2
n : ℕ
y : K
⊢ R K p (x.fst + (n, y).fst, (↑(frobenius K p)^[(n, y).fst]) x.snd + (↑(frobenius K p)^[x.fst]) (n, y).snd)
    (x.fst + (n + 1, ↑(frobenius K p) y).fst,
      ↑(frobenius K p) ((↑(frobenius K p)^[n]) x.snd + (↑(frobenius K p)^[x.fst]) y))
apply R.intro