theorem coprime_add_self_pow {R : Type u_1} [CommRing R] {x : R} {y : R} {z : R} {n : ℕ} (hn : 0 < n) (hsoln : x ^ n + y ^ n = z ^ n) (hxx : IsCoprime x y) : IsCoprime x z

theorem Int.factor_div (a : ℤ) (x : ℤ) (hodd : Odd x) : ∃ m c, c + m * x = a ∧ 2 * Int.natAbs c < Int.natAbs x

theorem two_not_cube (r : ℕ) : r ^ 3 ≠ 2

theorem Int.two_not_cube (r : ℤ) : r ^ 3 ≠ 2

theorem Irreducible.coprime_of_not_dvd_of_dvd {R : Type u_1} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [GCDMonoid R] {p : R} {k : R} {m : R} (hp : Irreducible p) (hdvd1 : ¬p ∣ m) (hdvd2 : k ∣ m) : IsCoprime p k

theorem Irreducible.dvd_of_dvd_mul_left {R : Type u_1} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [GCDMonoid R] {p : R} {k : R} {m : R} {n : R} (hdvd1 : ¬p ∣ m) (hdvd2 : k ∣ m) (hp : Irreducible p) (h : k ∣ p * n) : k ∣ n

theorem Int.dvd_mul_cancel_prime' {p : ℤ} {k : ℤ} {m : ℤ} {n : ℤ} (hdvd1 : ¬p ∣ m) (hdvd2 : k ∣ m) (hp : Prime p) (h : k ∣ p * n) : k ∣ n