no goals
K : Type u
inst✝³ : CommRing K
inst✝² : IsDomain K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ × K
x✝ : ∃ z, (↑(frobenius K p)^[y.fst + z]) x.snd = (↑(frobenius K p)^[x.fst + z]) y.snd
z : ℕ
H : (↑(frobenius K p)^[y.fst + z]) x.snd = (↑(frobenius K p)^[x.fst + z]) y.snd
⊢ (↑(frobenius K p)^[z]) ((↑(frobenius K p)^[y.fst]) x.snd) = (↑(frobenius K p)^[z]) ((↑(frobenius K p)^[x.fst]) y.snd)
simpa only [add_comm, iterate_add] using H