s : ℕ
h : s ≠ 0
⊢ (xgcdAux s 1 0 0 0 1).snd.snd = 0
s : ℕ
h : s ≠ 0
⊢ gcdB s 0 = 0
unfold gcdB xgcd
case intro
s : ℕ
h : succ s ≠ 0
⊢ (xgcdAux (succ s) 1 0 0 0 1).snd.snd = 0
s : ℕ
h : s ≠ 0
⊢ (xgcdAux s 1 0 0 0 1).snd.snd = 0
obtain ⟨s, rfl⟩ := Nat.exists_eq_succ_of_ne_zero h
case intro
s : ℕ
h : succ s ≠ 0
⊢ (xgcdAux (0 % succ s) (0 - ↑0 / ↑(succ s) * 1) (1 - ↑0 / ↑(succ s) * 0) (succ s) 1 0).snd.snd = 0
case intro
s : ℕ
h : succ s ≠ 0
⊢ (xgcdAux (succ s) 1 0 0 0 1).snd.snd = 0
rw [xgcdAux_succ]
no goals
case intro
s : ℕ
h : succ s ≠ 0
⊢ (xgcdAux (0 % succ s) (0 - ↑0 / ↑(succ s) * 1) (1 - ↑0 / ↑(succ s) * 0) (succ s) 1 0).snd.snd = 0
rfl