u : XgcdType
⊢ u.wp + u.zp + u.wp * u.zp = u.x * u.y ↔ w u * z u = succPNat (u.x * u.y)
u : XgcdType
⊢ IsSpecial u ↔ IsSpecial' u
dsimp [IsSpecial, IsSpecial']
u : XgcdType
wp x y zp ap bp : ℕ
⊢ { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp +
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp +
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp =
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y ↔
    w { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp } *
        z { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp } =
      succPNat
        ({ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y)
u : XgcdType
⊢ u.wp + u.zp + u.wp * u.zp = u.x * u.y ↔ w u * z u = succPNat (u.x * u.y)
let ⟨wp, x, y, zp, ap, bp⟩ := u
case mp
u : XgcdType
wp x y zp ap bp : ℕ
h : wp + zp + wp * zp = x * y
⊢ succ wp * succ zp = succ (x * y)

case mpr
u : XgcdType
wp x y zp ap bp : ℕ
h : succ wp * succ zp = succ (x * y)
⊢ wp + zp + wp * zp = x * y
u : XgcdType
wp x y zp ap bp : ℕ
⊢ { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp +
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp +
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp =
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y ↔
    w { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp } *
        z { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp } =
      succPNat
        ({ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y)
constructor <;> intro h <;> simp [w, z, succPNat] at * <;>
  simp only [← coe_inj, mul_coe, mk_coe] at *
case mpr
u : XgcdType
wp x y zp ap bp : ℕ
h : succ wp * succ zp = succ (x * y)
⊢ wp + zp + wp * zp = x * y
case mp
u : XgcdType
wp x y zp ap bp : ℕ
h : wp + zp + wp * zp = x * y
⊢ succ wp * succ zp = succ (x * y)

case mpr
u : XgcdType
wp x y zp ap bp : ℕ
h : succ wp * succ zp = succ (x * y)
⊢ wp + zp + wp * zp = x * y
. simp_all [← h, Nat.mul, Nat.succ_eq_add_one]; ring
no goals
case mpr
u : XgcdType
wp x y zp ap bp : ℕ
h : succ wp * succ zp = succ (x * y)
⊢ wp + zp + wp * zp = x * y
. simp [Nat.succ_eq_add_one, Nat.mul_add, Nat.add_mul, ← Nat.add_assoc] at h; rw [← h]; ring
case mp
u : XgcdType
wp x y zp ap bp : ℕ
⊢ (wp + 1) * (zp + 1) = wp + zp + wp * zp + 1
case mp
u : XgcdType
wp x y zp ap bp : ℕ
h : wp + zp + wp * zp = x * y
⊢ succ wp * succ zp = succ (x * y)
simp_all [← h, Nat.mul, Nat.succ_eq_add_one]
no goals
case mp
u : XgcdType
wp x y zp ap bp : ℕ
⊢ (wp + 1) * (zp + 1) = wp + zp + wp * zp + 1
ring
case mpr
u : XgcdType
wp x y zp ap bp : ℕ
h : wp * zp + zp + wp = x * y
⊢ wp + zp + wp * zp = x * y
case mpr
u : XgcdType
wp x y zp ap bp : ℕ
h : succ wp * succ zp = succ (x * y)
⊢ wp + zp + wp * zp = x * y
simp [Nat.succ_eq_add_one, Nat.mul_add, Nat.add_mul, ← Nat.add_assoc] at h
case mpr
u : XgcdType
wp x y zp ap bp : ℕ
h : wp * zp + zp + wp = x * y
⊢ wp + zp + wp * zp = wp * zp + zp + wp
case mpr
u : XgcdType
wp x y zp ap bp : ℕ
h : wp * zp + zp + wp = x * y
⊢ wp + zp + wp * zp = x * y
rw [← h]
no goals
case mpr
u : XgcdType
wp x y zp ap bp : ℕ
h : wp * zp + zp + wp = x * y
⊢ wp + zp + wp * zp = wp * zp + zp + wp
ring