R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s : R
⊢ (xgcd 0 s).snd = 1
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s : R
⊢ gcdB 0 s = 1
unfold gcdB
no goals
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s : R
⊢ (xgcd 0 s).snd = 1
rw [xgcd, xgcd_zero_left]