case intro
s t : ℤ
r' : ℕ
s' t' : ℤ
r : ℕ
h : 0 < succ r
⊢ xgcdAux (succ r) s t r' s' t' =
    xgcdAux (r' % succ r) (s' - ↑r' / ↑(succ r) * s) (t' - ↑r' / ↑(succ r) * t) (succ r) s t
r : ℕ
s t : ℤ
r' : ℕ
s' t' : ℤ
h : 0 < r
⊢ xgcdAux r s t r' s' t' = xgcdAux (r' % r) (s' - ↑r' / ↑r * s) (t' - ↑r' / ↑r * t) r s t
obtain ⟨r, rfl⟩ := Nat.exists_eq_succ_of_ne_zero h.ne'
no goals
case intro
s t : ℤ
r' : ℕ
s' t' : ℤ
r : ℕ
h : 0 < succ r
⊢ xgcdAux (succ r) s t r' s' t' =
    xgcdAux (r' % succ r) (s' - ↑r' / ↑(succ r) * s) (t' - ↑r' / ↑(succ r) * t) (succ r) s t
rfl