x y : ℕ
this : Nat.P x y (xgcdAux x 1 0 y 0 1)
⊢ ↑(gcd x y) = ↑x * gcdA x y + ↑y * gcdB x y
x y : ℕ
⊢ ↑(gcd x y) = ↑x * gcdA x y + ↑y * gcdB x y
have := @xgcd_aux_P x y x y 1 0 0 1 (by simp [P]) (by simp [P])
no goals
x y : ℕ
this : Nat.P x y (xgcdAux x 1 0 y 0 1)
⊢ ↑(gcd x y) = ↑x * gcdA x y + ↑y * gcdB x y
rwa [xgcd_aux_val, xgcd_val] at this
no goals
x y : ℕ
⊢ Nat.P x y (x, 1, 0)
simp [P]
no goals
x y : ℕ
⊢ Nat.P x y (y, 0, 1)
simp [P]