x y : ℤ
d : ℕ
hd : Int.gcd x y = d
h : Nat.beq d 1 = false
⊢ ¬d = 1
x y : ℤ
d : ℕ
hd : Int.gcd x y = d
h : Nat.beq d 1 = false
⊢ ¬IsCoprime x y
rw [Int.isCoprime_iff_gcd_eq_one, hd]
no goals
x y : ℤ
d : ℕ
hd : Int.gcd x y = d
h : Nat.beq d 1 = false
⊢ ¬d = 1
exact Nat.ne_of_beq_eq_false h