u : XgcdType
hs : u.wp + u.zp + u.wp * u.zp = u.x * u.y
⊢ u.wp + (u.y * qp u + u.zp) + u.wp * (u.y * qp u + u.zp) = ((u.wp + 1) * qp u + u.x) * u.y
u : XgcdType
hs : IsSpecial u
⊢ IsSpecial (finish u)
dsimp [IsSpecial, finish] at hs⊢
u : XgcdType
hs : u.wp + u.zp + u.wp * u.zp = u.x * u.y
⊢ u.wp + (u.y * qp u + u.zp) + u.wp * (u.y * qp u + u.zp) = u.wp + u.zp + u.wp * u.zp + (u.wp + 1) * qp u * u.y
u : XgcdType
hs : u.wp + u.zp + u.wp * u.zp = u.x * u.y
⊢ u.wp + (u.y * qp u + u.zp) + u.wp * (u.y * qp u + u.zp) = ((u.wp + 1) * qp u + u.x) * u.y
rw [add_mul _ _ u.y, add_comm _ (u.x * u.y), ← hs]
no goals
u : XgcdType
hs : u.wp + u.zp + u.wp * u.zp = u.x * u.y
⊢ u.wp + (u.y * qp u + u.zp) + u.wp * (u.y * qp u + u.zp) = u.wp + u.zp + u.wp * u.zp + (u.wp + 1) * qp u * u.y
ring