Comment by throw46395

    import FLT 
    theorem PNat.pow_add_pow_ne_pow
        (x y z : ℕ+)
        (n : ℕ) (hn : n > 2) :
        x^n + y^n ≠ z^n := PNat.pow_add_pow_ne_pow_of_FermatLastTheorem FLT.Wiles_Taylor_Wiles x y z n hn