u : XgcdType
⊢ u.zp + u.wp + u.zp * u.wp = u.y * u.x ↔ u.wp + u.zp + u.wp * u.zp = u.x * u.y
u : XgcdType
⊢ IsSpecial (flip u) ↔ IsSpecial u
dsimp [IsSpecial, flip]
no goals
u : XgcdType
⊢ u.zp + u.wp + u.zp * u.wp = u.y * u.x ↔ u.wp + u.zp + u.wp * u.zp = u.x * u.y
rw [mul_comm u.x, mul_comm u.zp, add_comm u.zp]