x y : ℕ
⊢ xgcd x y = ((xgcd x y).fst, (xgcd x y).snd)
x y : ℕ
⊢ xgcd x y = (gcdA x y, gcdB x y)
unfold gcdA gcdB
case mk
x y : ℕ
fst✝ snd✝ : ℤ
⊢ (fst✝, snd✝) = ((fst✝, snd✝).fst, (fst✝, snd✝).snd)
x y : ℕ
⊢ xgcd x y = ((xgcd x y).fst, (xgcd x y).snd)
cases xgcd x y
no goals
case mk
x y : ℕ
fst✝ snd✝ : ℤ
⊢ (fst✝, snd✝) = ((fst✝, snd✝).fst, (fst✝, snd✝).snd)
rfl