n : ℕ
⊢ ↑(Nat.gcdA 0 (n + 1)) = 0
n : ℕ
⊢ ↑(Nat.gcdA (val 0) (n + 1)) = 0
rw [val_zero]
n : ℕ
⊢ ↑(n + 1, 0, 1).snd.fst = 0
n : ℕ
⊢ ↑(Nat.gcdA 0 (n + 1)) = 0
unfold Nat.gcdA Nat.xgcd Nat.xgcdAux
no goals
n : ℕ
⊢ ↑(n + 1, 0, 1).snd.fst = 0
rfl