R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y x✝ s✝ t✝ s'✝ t'✝ : R
⊢ (xgcdAux 0 s✝ t✝ x✝ s'✝ t'✝).fst = gcd 0 x✝
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
⊢ ∀ (x s t s' t' : R), (xgcdAux 0 s t x s' t').fst = gcd 0 x
intros
no goals
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y x✝ s✝ t✝ s'✝ t'✝ : R
⊢ (xgcdAux 0 s✝ t✝ x✝ s'✝ t'✝).fst = gcd 0 x✝
rw [xgcd_zero_left, gcd_zero_left]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x✝ y✝ x y : R
h : x ≠ 0
IH : ∀ (s t s' t' : R), (xgcdAux (y % x) s t x s' t').fst = gcd (y % x) x
s t s' t' : R
⊢ gcd (y % x) x = gcd x y
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x✝ y✝ x y : R
h : x ≠ 0
IH : ∀ (s t s' t' : R), (xgcdAux (y % x) s t x s' t').fst = gcd (y % x) x
s t s' t' : R
⊢ (xgcdAux x s t y s' t').fst = gcd x y
simp only [xgcdAux_rec h, if_neg h, IH]
no goals
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x✝ y✝ x y : R
h : x ≠ 0
IH : ∀ (s t s' t' : R), (xgcdAux (y % x) s t x s' t').fst = gcd (y % x) x
s t s' t' : R
⊢ gcd (y % x) x = gcd x y
rw [← gcd_val]