rwa [mul_one, hsoln, IsCoprime.pow_iff hn hn] at this
R : Type u_1
inst✝ : CommRing R
x y z : R
n : ℕ
hn : 0 < n
hsoln : x ^ n + y ^ n = z ^ n
hxx : IsCoprime x y
this : IsCoprime (x ^ n) (x ^ n * 1 + y ^ n)
⊢ IsCoprime x z
no goals