x y : ℤ
⊢ Int.gcd x y = Nat.gcd (Int.natAbs x) (Int.natAbs y)
x y : ℤ
x' y' d : ℕ
hx : Int.natAbs x = x'
hy : Int.natAbs y = y'
h : Nat.gcd x' y' = d
⊢ Int.gcd x y = d
subst_vars
no goals
x y : ℤ
⊢ Int.gcd x y = Nat.gcd (Int.natAbs x) (Int.natAbs y)
rw [Int.gcd_def]