R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
r s t r' s' t' : R
h : 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' =
    xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
r s t r' s' t' : R
h : r ≠ 0
⊢ xgcdAux r s t r' s' t' = xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t
conv =>
  lhs
  rw [xgcdAux]
no goals
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
r s t r' s' t' : R
h : 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' =
    xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t
exact if_neg h