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