no goals
x y : ℕ
⊢ ∀ (n : ℕ) (s t s' t' : ℤ), (xgcdAux 0 s t n s' t').fst = gcd 0 n
simp
x✝ y✝ x y : ℕ
h : 0 < x
IH : ∀ (s t s' t' : ℤ), (xgcdAux (y % x) s t x s' t').fst = gcd (y % x) x
s t s' t' : ℤ
⊢ gcd (y % x) x = gcd x y
x✝ y✝ x y : ℕ
h : 0 < x
IH : ∀ (s t s' t' : ℤ), (xgcdAux (y % x) s t x s' t').fst = gcd (y % x) x
s t s' t' : ℤ
⊢ (xgcdAux x s t y s' t').fst = gcd x y
simp [xgcd_aux_rec, h, IH]
no goals
x✝ y✝ x y : ℕ
h : 0 < x
IH : ∀ (s t s' t' : ℤ), (xgcdAux (y % x) s t x s' t').fst = gcd (y % x) x
s t s' t' : ℤ
⊢ gcd (y % x) x = gcd x y
rw [← gcd_rec]