R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s t r' s' t' : R
⊢ (let r := 0;
      fun s t r' s' t' =>
      if _hr : r = 0 then (r', s', t')
      else
        let q := r' / r;
        xgcdAux (r' % r) (s' - q * s) (t' - q * t) r s t)
      s t r' s' t' =
    (r', s', t')
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s t r' s' t' : R
⊢ xgcdAux 0 s t r' s' t' = (r', s', t')
unfold xgcdAux
no goals
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s t r' s' t' : R
⊢ (let r := 0;
      fun s t r' s' t' =>
      if _hr : r = 0 then (r', s', t')
      else
        let q := r' / r;
        xgcdAux (r' % r) (s' - q * s) (t' - q * t) r s t)
      s t r' s' t' =
    (r', s', t')
exact if_pos rfl