u : XgcdType
hs : u.wp + u.zp + u.wp * u.zp = u.x * u.y
⊢ u.y * q u + u.zp + u.wp + (u.y * q u + u.zp) * u.wp = u.y * ((u.wp + 1) * q u + u.x)
u : XgcdType
hs : IsSpecial u
⊢ IsSpecial (step u)
dsimp [IsSpecial, step] at hs⊢
u : XgcdType
hs : u.wp + u.zp + u.wp * u.zp = u.x * u.y
⊢ u.y * q u + u.zp + u.wp + (u.y * q u + u.zp) * u.wp = u.y * ((u.wp + 1) * q u) + (u.wp + u.zp + u.wp * u.zp)
u : XgcdType
hs : u.wp + u.zp + u.wp * u.zp = u.x * u.y
⊢ u.y * q u + u.zp + u.wp + (u.y * q u + u.zp) * u.wp = u.y * ((u.wp + 1) * q u + u.x)
rw [mul_add, mul_comm u.y u.x, ← hs]
no goals
u : XgcdType
hs : u.wp + u.zp + u.wp * u.zp = u.x * u.y
⊢ u.y * q u + u.zp + u.wp + (u.y * q u + u.zp) * u.wp = u.y * ((u.wp + 1) * q u) + (u.wp + u.zp + u.wp * u.zp)
ring