R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
this : EuclideanDomain.P a b (xgcdAux a 1 0 b 0 1)
⊢ gcd a b = a * gcdA a b + b * gcdB a b
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ gcd a b = a * gcdA a b + b * gcdB a b
have :=
  @xgcdAux_P _ _ _ a b a b 1 0 0 1 (by dsimp [P]; rw [mul_one, mul_zero, add_zero])
    (by dsimp [P]; rw [mul_one, mul_zero, zero_add])
no goals
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
this : EuclideanDomain.P a b (xgcdAux a 1 0 b 0 1)
⊢ gcd a b = a * gcdA a b + b * gcdB a b
rwa [xgcdAux_val, xgcd_val] at this
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ a = a * 1 + b * 0
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ EuclideanDomain.P a b (a, 1, 0)
dsimp [P]
no goals
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ a = a * 1 + b * 0
rw [mul_one, mul_zero, add_zero]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ b = a * 0 + b * 1
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ EuclideanDomain.P a b (b, 0, 1)
dsimp [P]
no goals
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ b = a * 0 + b * 1
rw [mul_one, mul_zero, zero_add]