a b : ℕ+
⊢ succ ((xgcd a b).y + (xgcd a b).zp) = (xgcd a b).y + succ (xgcd a b).zp
a b : ℕ+
⊢ ↑(gcdB' a b) = gcdY a b + ↑(gcdZ a b)
dsimp [gcdB', gcdY, gcdZ, XgcdType.z]
no goals
a b : ℕ+
⊢ succ ((xgcd a b).y + (xgcd a b).zp) = (xgcd a b).y + succ (xgcd a b).zp
rw [Nat.succ_eq_add_one, Nat.succ_eq_add_one, add_assoc]