no goals
u : XgcdType
⊢ v u = succ₂ (vp u)
ext <;> dsimp [v, vp, w, z, a, b, succ₂] <;> (repeat' rw [Nat.succ_eq_add_one]; ring_nf)
no goals
case h₂
u : XgcdType
⊢ u.y * succ u.ap + succ u.zp * succ u.bp = succ (u.y + u.zp + u.bp + u.y * u.ap + u.zp * u.bp)
repeat' rw [Nat.succ_eq_add_one]; ring_nf
case h₂
u : XgcdType
⊢ 1 + u.y + u.y * u.ap + u.zp + u.zp * u.bp + u.bp = u.y + u.y * u.ap + u.zp + u.zp * u.bp + u.bp + 1
case h₂
u : XgcdType
⊢ 1 + u.y + u.y * u.ap + u.zp + u.zp * u.bp + u.bp = succ (u.y + u.y * u.ap + u.zp + u.zp * u.bp + u.bp)
rw [Nat.succ_eq_add_one]
no goals
case h₂
u : XgcdType
⊢ 1 + u.y + u.y * u.ap + u.zp + u.zp * u.bp + u.bp = u.y + u.y * u.ap + u.zp + u.zp * u.bp + u.bp + 1
ring_nf