[GOAL]
u : XgcdType
⊢ v u = succ₂ (vp u)
[PROOFSTEP]
ext
[GOAL]
case h₁
u : XgcdType
⊢ (v u).fst = (succ₂ (vp u)).fst
[PROOFSTEP]
dsimp [v, vp, w, z, a, b, succ₂]
[GOAL]
case h₂
u : XgcdType
⊢ (v u).snd = (succ₂ (vp u)).snd
[PROOFSTEP]
dsimp [v, vp, w, z, a, b, succ₂]
[GOAL]
case h₁
u : XgcdType
⊢ succ u.wp * succ u.ap + u.x * succ u.bp = succ (u.wp + u.x + u.ap + u.wp * u.ap + u.x * u.bp)
[PROOFSTEP]
repeat' rw [Nat.succ_eq_add_one]; ring_nf
[GOAL]
case h₁
u : XgcdType
⊢ succ u.wp * succ u.ap + u.x * succ u.bp = succ (u.wp + u.x + u.ap + u.wp * u.ap + u.x * u.bp)
[PROOFSTEP]
rw [Nat.succ_eq_add_one]
[GOAL]
case h₁
u : XgcdType
⊢ (u.wp + 1) * succ u.ap + u.x * succ u.bp = succ (u.wp + u.x + u.ap + u.wp * u.ap + u.x * u.bp)
[PROOFSTEP]
ring_nf
[GOAL]
case h₁
u : XgcdType
⊢ u.wp * succ u.ap + succ u.ap + u.x * succ u.bp = succ (u.wp + u.wp * u.ap + u.x + u.x * u.bp + u.ap)
[PROOFSTEP]
rw [Nat.succ_eq_add_one]
[GOAL]
case h₁
u : XgcdType
⊢ u.wp * (u.ap + 1) + (u.ap + 1) + u.x * succ u.bp = succ (u.wp + u.wp * u.ap + u.x + u.x * u.bp + u.ap)
[PROOFSTEP]
ring_nf
[GOAL]
case h₁
u : XgcdType
⊢ 1 + u.wp + u.wp * u.ap + u.ap + u.x * succ u.bp = succ (u.wp + u.wp * u.ap + u.ap + u.x + u.x * u.bp)
[PROOFSTEP]
rw [Nat.succ_eq_add_one]
[GOAL]
case h₁
u : XgcdType
⊢ 1 + u.wp + u.wp * u.ap + u.ap + u.x * (u.bp + 1) = succ (u.wp + u.wp * u.ap + u.ap + u.x + u.x * u.bp)
[PROOFSTEP]
ring_nf
[GOAL]
case h₁
u : XgcdType
⊢ 1 + u.wp + u.wp * u.ap + u.ap + u.x + u.x * u.bp = succ (u.wp + u.wp * u.ap + u.ap + u.x + u.x * u.bp)
[PROOFSTEP]
rw [Nat.succ_eq_add_one]
[GOAL]
case h₁
u : XgcdType
⊢ 1 + u.wp + u.wp * u.ap + u.ap + u.x + u.x * u.bp = u.wp + u.wp * u.ap + u.ap + u.x + u.x * u.bp + 1
[PROOFSTEP]
ring_nf
[GOAL]
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)
[PROOFSTEP]
repeat' rw [Nat.succ_eq_add_one]; ring_nf
[GOAL]
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)
[PROOFSTEP]
rw [Nat.succ_eq_add_one]
[GOAL]
case h₂
u : XgcdType
⊢ u.y * (u.ap + 1) + succ u.zp * succ u.bp = succ (u.y + u.zp + u.bp + u.y * u.ap + u.zp * u.bp)
[PROOFSTEP]
ring_nf
[GOAL]
case h₂
u : XgcdType
⊢ u.y + u.y * u.ap + succ u.zp * succ u.bp = succ (u.y + u.y * u.ap + u.zp + u.zp * u.bp + u.bp)
[PROOFSTEP]
rw [Nat.succ_eq_add_one]
[GOAL]
case h₂
u : XgcdType
⊢ u.y + u.y * u.ap + (u.zp + 1) * succ u.bp = succ (u.y + u.y * u.ap + u.zp + u.zp * u.bp + u.bp)
[PROOFSTEP]
ring_nf
[GOAL]
case h₂
u : XgcdType
⊢ u.y + u.y * u.ap + u.zp * succ u.bp + succ u.bp = succ (u.y + u.y * u.ap + u.zp + u.zp * u.bp + u.bp)
[PROOFSTEP]
rw [Nat.succ_eq_add_one]
[GOAL]
case h₂
u : XgcdType
⊢ u.y + u.y * u.ap + u.zp * (u.bp + 1) + (u.bp + 1) = succ (u.y + u.y * u.ap + u.zp + u.zp * u.bp + u.bp)
[PROOFSTEP]
ring_nf
[GOAL]
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)
[PROOFSTEP]
rw [Nat.succ_eq_add_one]
[GOAL]
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
[PROOFSTEP]
ring_nf
[GOAL]
u : XgcdType
⊢ IsSpecial u ↔ IsSpecial' u
[PROOFSTEP]
dsimp [IsSpecial, IsSpecial']
[GOAL]
u : XgcdType
⊢ u.wp + u.zp + u.wp * u.zp = u.x * u.y ↔ w u * z u = succPNat (u.x * u.y)
[PROOFSTEP]
let ⟨wp, x, y, zp, ap, bp⟩ := u
[GOAL]
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)
[PROOFSTEP]
constructor
[GOAL]
case mp
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)
[PROOFSTEP]
intro h
[GOAL]
case mpr
u : XgcdType
wp x y zp ap bp : ℕ
⊢ 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) →
    { 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
[PROOFSTEP]
intro h
[GOAL]
case mp
u : XgcdType
wp x y zp ap bp : ℕ
h :
  { 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)
[PROOFSTEP]
simp [w, z, succPNat] at *
[GOAL]
case mpr
u : XgcdType
wp x y zp ap bp : ℕ
h :
  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)
⊢ { 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
[PROOFSTEP]
simp [w, z, succPNat] at *
[GOAL]
case mp
u : XgcdType
wp x y zp ap bp : ℕ
h : wp + zp + wp * zp = x * y
⊢ { val := succ wp, property := (_ : 0 < succ { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp) } *
      { val := succ zp, property := (_ : 0 < succ { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp) } =
    { val := succ (x * y),
      property :=
        (_ :
          0 <
            succ
              ({ 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)) }
[PROOFSTEP]
simp only [← coe_inj, mul_coe, mk_coe] at *
[GOAL]
case mpr
u : XgcdType
wp x y zp ap bp : ℕ
h :
  { val := succ wp, property := (_ : 0 < succ { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp) } *
      { val := succ zp, property := (_ : 0 < succ { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp) } =
    { val := succ (x * y),
      property :=
        (_ :
          0 <
            succ
              ({ 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)) }
⊢ wp + zp + wp * zp = x * y
[PROOFSTEP]
simp only [← coe_inj, mul_coe, mk_coe] at *
[GOAL]
case mp
u : XgcdType
wp x y zp ap bp : ℕ
h : wp + zp + wp * zp = x * y
⊢ succ wp * succ zp = succ (x * y)
[PROOFSTEP]
simp_all [← h, Nat.mul, Nat.succ_eq_add_one]
[GOAL]
case mp
u : XgcdType
wp x y zp ap bp : ℕ
⊢ (wp + 1) * (zp + 1) = wp + zp + wp * zp + 1
[PROOFSTEP]
ring
[GOAL]
case mpr
u : XgcdType
wp x y zp ap bp : ℕ
h : succ wp * succ zp = succ (x * y)
⊢ wp + zp + wp * zp = x * y
[PROOFSTEP]
simp [Nat.succ_eq_add_one, Nat.mul_add, Nat.add_mul, ← Nat.add_assoc] at h 
[GOAL]
case mpr
u : XgcdType
wp x y zp ap bp : ℕ
h : wp * zp + zp + wp = x * y
⊢ wp + zp + wp * zp = x * y
[PROOFSTEP]
rw [← h]
[GOAL]
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
[PROOFSTEP]
ring
  -- Porting note: Old code has been removed as it was much more longer.
[GOAL]
u : XgcdType
⊢ IsReduced (flip u) ↔ IsReduced u
[PROOFSTEP]
dsimp [IsReduced, flip]
[GOAL]
u : XgcdType
⊢ u.bp = u.ap ↔ u.ap = u.bp
[PROOFSTEP]
constructor
[GOAL]
case mp
u : XgcdType
⊢ u.bp = u.ap → u.ap = u.bp
[PROOFSTEP]
intro h
[GOAL]
case mpr
u : XgcdType
⊢ u.ap = u.bp → u.bp = u.ap
[PROOFSTEP]
intro h
[GOAL]
case mp
u : XgcdType
h : u.bp = u.ap
⊢ u.ap = u.bp
[PROOFSTEP]
exact h.symm
[GOAL]
case mpr
u : XgcdType
h : u.ap = u.bp
⊢ u.bp = u.ap
[PROOFSTEP]
exact h.symm
[GOAL]
u : XgcdType
⊢ IsSpecial (flip u) ↔ IsSpecial u
[PROOFSTEP]
dsimp [IsSpecial, flip]
[GOAL]
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
[PROOFSTEP]
rw [mul_comm u.x, mul_comm u.zp, add_comm u.zp]
[GOAL]
u : XgcdType
⊢ v (flip u) = Prod.swap (v u)
[PROOFSTEP]
dsimp [v]
[GOAL]
u : XgcdType
⊢ (↑(z u) * ↑(b u) + u.y * ↑(a u), u.x * ↑(b u) + ↑(w u) * ↑(a u)) =
    (u.y * ↑(a u) + ↑(z u) * ↑(b u), ↑(w u) * ↑(a u) + u.x * ↑(b u))
[PROOFSTEP]
ext
[GOAL]
case h₁
u : XgcdType
⊢ (↑(z u) * ↑(b u) + u.y * ↑(a u), u.x * ↑(b u) + ↑(w u) * ↑(a u)).fst =
    (u.y * ↑(a u) + ↑(z u) * ↑(b u), ↑(w u) * ↑(a u) + u.x * ↑(b u)).fst
[PROOFSTEP]
simp only
[GOAL]
case h₁
u : XgcdType
⊢ ↑(z u) * ↑(b u) + u.y * ↑(a u) = u.y * ↑(a u) + ↑(z u) * ↑(b u)
[PROOFSTEP]
ring
[GOAL]
case h₂
u : XgcdType
⊢ (↑(z u) * ↑(b u) + u.y * ↑(a u), u.x * ↑(b u) + ↑(w u) * ↑(a u)).snd =
    (u.y * ↑(a u) + ↑(z u) * ↑(b u), ↑(w u) * ↑(a u) + u.x * ↑(b u)).snd
[PROOFSTEP]
simp only
[GOAL]
case h₂
u : XgcdType
⊢ u.x * ↑(b u) + ↑(w u) * ↑(a u) = ↑(w u) * ↑(a u) + u.x * ↑(b u)
[PROOFSTEP]
ring
[GOAL]
u : XgcdType
hr : r u = 0
⊢ q u = qp u + 1
[PROOFSTEP]
by_cases hq : u.q = 0
[GOAL]
case pos
u : XgcdType
hr : r u = 0
hq : q u = 0
⊢ q u = qp u + 1
[PROOFSTEP]
let h := u.rq_eq
[GOAL]
case pos
u : XgcdType
hr : r u = 0
hq : q u = 0
h : r u + (u.bp + 1) * q u = u.ap + 1 := rq_eq u
⊢ q u = qp u + 1
[PROOFSTEP]
rw [hr, hq, mul_zero, add_zero] at h 
[GOAL]
case pos
u : XgcdType
hr : r u = 0
hq : q u = 0
h : 0 = u.ap + 1
⊢ q u = qp u + 1
[PROOFSTEP]
cases h
[GOAL]
case neg
u : XgcdType
hr : r u = 0
hq : ¬q u = 0
⊢ q u = qp u + 1
[PROOFSTEP]
exact (Nat.succ_pred_eq_of_pos (Nat.pos_of_ne_zero hq)).symm
[GOAL]
u : XgcdType
a b : ℕ+
⊢ IsSpecial (start a b)
[PROOFSTEP]
dsimp [start, IsSpecial]
[GOAL]
u : XgcdType
a b : ℕ+
⊢ v (start a b) = (↑a, ↑b)
[PROOFSTEP]
dsimp [start, v, XgcdType.a, XgcdType.b, w, z]
[GOAL]
u : XgcdType
a b : ℕ+
⊢ (succ 0 * succ (↑a - 1) + 0 * succ (↑b - 1), 0 * succ (↑a - 1) + succ 0 * succ (↑b - 1)) = (↑a, ↑b)
[PROOFSTEP]
have : succ 0 = 1 := rfl
[GOAL]
u : XgcdType
a b : ℕ+
this : succ 0 = 1
⊢ (succ 0 * succ (↑a - 1) + 0 * succ (↑b - 1), 0 * succ (↑a - 1) + succ 0 * succ (↑b - 1)) = (↑a, ↑b)
[PROOFSTEP]
rw [this, one_mul, one_mul, zero_mul, zero_mul, zero_add, add_zero]
[GOAL]
u : XgcdType
a b : ℕ+
this : succ 0 = 1
⊢ (succ (↑a - 1), succ (↑b - 1)) = (↑a, ↑b)
[PROOFSTEP]
rw [← Nat.pred_eq_sub_one, ← Nat.pred_eq_sub_one]
[GOAL]
u : XgcdType
a b : ℕ+
this : succ 0 = 1
⊢ (succ (pred ↑a), succ (pred ↑b)) = (↑a, ↑b)
[PROOFSTEP]
rw [Nat.succ_pred_eq_of_pos a.pos, Nat.succ_pred_eq_of_pos b.pos]
[GOAL]
u : XgcdType
⊢ IsReduced (finish u)
[PROOFSTEP]
dsimp [IsReduced]
[GOAL]
u : XgcdType
⊢ (finish u).ap = (finish u).bp
[PROOFSTEP]
rfl
[GOAL]
u : XgcdType
hs : IsSpecial u
⊢ IsSpecial (finish u)
[PROOFSTEP]
dsimp [IsSpecial, finish] at hs ⊢
[GOAL]
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
[PROOFSTEP]
rw [add_mul _ _ u.y, add_comm _ (u.x * u.y), ← hs]
[GOAL]
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
[PROOFSTEP]
ring
[GOAL]
u : XgcdType
hr : r u = 0
⊢ v (finish u) = v u
[PROOFSTEP]
let ha : u.r + u.b * u.q = u.a := u.rq_eq
[GOAL]
u : XgcdType
hr : r u = 0
ha : r u + ↑(b u) * q u = ↑(a u) := rq_eq u
⊢ v (finish u) = v u
[PROOFSTEP]
rw [hr, zero_add] at ha 
[GOAL]
u : XgcdType
hr : r u = 0
ha : ↑(b u) * q u = ↑(a u)
⊢ v (finish u) = v u
[PROOFSTEP]
ext
[GOAL]
case h₁
u : XgcdType
hr : r u = 0
ha : ↑(b u) * q u = ↑(a u)
⊢ (v (finish u)).fst = (v u).fst
[PROOFSTEP]
change (u.wp + 1) * u.b + ((u.wp + 1) * u.qp + u.x) * u.b = u.w * u.a + u.x * u.b
[GOAL]
case h₁
u : XgcdType
hr : r u = 0
ha : ↑(b u) * q u = ↑(a u)
⊢ (u.wp + 1) * ↑(b u) + ((u.wp + 1) * qp u + u.x) * ↑(b u) = ↑(w u) * ↑(a u) + u.x * ↑(b u)
[PROOFSTEP]
have : u.wp + 1 = u.w := rfl
[GOAL]
case h₁
u : XgcdType
hr : r u = 0
ha : ↑(b u) * q u = ↑(a u)
this : u.wp + 1 = ↑(w u)
⊢ (u.wp + 1) * ↑(b u) + ((u.wp + 1) * qp u + u.x) * ↑(b u) = ↑(w u) * ↑(a u) + u.x * ↑(b u)
[PROOFSTEP]
rw [this, ← ha, u.qp_eq hr]
[GOAL]
case h₁
u : XgcdType
hr : r u = 0
ha : ↑(b u) * q u = ↑(a u)
this : u.wp + 1 = ↑(w u)
⊢ ↑(w u) * ↑(b u) + (↑(w u) * qp u + u.x) * ↑(b u) = ↑(w u) * (↑(b u) * (qp u + 1)) + u.x * ↑(b u)
[PROOFSTEP]
ring
[GOAL]
case h₂
u : XgcdType
hr : r u = 0
ha : ↑(b u) * q u = ↑(a u)
⊢ (v (finish u)).snd = (v u).snd
[PROOFSTEP]
change u.y * u.b + (u.y * u.qp + u.z) * u.b = u.y * u.a + u.z * u.b
[GOAL]
case h₂
u : XgcdType
hr : r u = 0
ha : ↑(b u) * q u = ↑(a u)
⊢ u.y * ↑(b u) + (u.y * qp u + ↑(z u)) * ↑(b u) = u.y * ↑(a u) + ↑(z u) * ↑(b u)
[PROOFSTEP]
rw [← ha, u.qp_eq hr]
[GOAL]
case h₂
u : XgcdType
hr : r u = 0
ha : ↑(b u) * q u = ↑(a u)
⊢ u.y * ↑(b u) + (u.y * qp u + ↑(z u)) * ↑(b u) = u.y * (↑(b u) * (qp u + 1)) + ↑(z u) * ↑(b u)
[PROOFSTEP]
ring
[GOAL]
u : XgcdType
hr : r u ≠ 0
⊢ sizeOf (step u) < sizeOf u
[PROOFSTEP]
change u.r - 1 < u.bp
[GOAL]
u : XgcdType
hr : r u ≠ 0
⊢ r u - 1 < u.bp
[PROOFSTEP]
have h₀ : u.r - 1 + 1 = u.r := Nat.succ_pred_eq_of_pos (Nat.pos_of_ne_zero hr)
[GOAL]
u : XgcdType
hr : r u ≠ 0
h₀ : r u - 1 + 1 = r u
⊢ r u - 1 < u.bp
[PROOFSTEP]
have h₁ : u.r < u.bp + 1 := Nat.mod_lt (u.ap + 1) u.bp.succ_pos
[GOAL]
u : XgcdType
hr : r u ≠ 0
h₀ : r u - 1 + 1 = r u
h₁ : r u < u.bp + 1
⊢ r u - 1 < u.bp
[PROOFSTEP]
rw [← h₀] at h₁ 
[GOAL]
u : XgcdType
hr : r u ≠ 0
h₀ : r u - 1 + 1 = r u
h₁ : r u - 1 + 1 < u.bp + 1
⊢ r u - 1 < u.bp
[PROOFSTEP]
exact lt_of_succ_lt_succ h₁
[GOAL]
u : XgcdType
hs : IsSpecial u
⊢ IsSpecial (step u)
[PROOFSTEP]
dsimp [IsSpecial, step] at hs ⊢
[GOAL]
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)
[PROOFSTEP]
rw [mul_add, mul_comm u.y u.x, ← hs]
[GOAL]
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)
[PROOFSTEP]
ring
[GOAL]
u : XgcdType
hr : r u ≠ 0
⊢ v (step u) = Prod.swap (v u)
[PROOFSTEP]
let ha : u.r + u.b * u.q = u.a := u.rq_eq
[GOAL]
u : XgcdType
hr : r u ≠ 0
ha : r u + ↑(b u) * q u = ↑(a u) := rq_eq u
⊢ v (step u) = Prod.swap (v u)
[PROOFSTEP]
let hr : u.r - 1 + 1 = u.r := (add_comm _ 1).trans (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr))
[GOAL]
u : XgcdType
hr✝ : r u ≠ 0
ha : r u + ↑(b u) * q u = ↑(a u) := rq_eq u
hr : r u - 1 + 1 = r u := Eq.trans (add_comm (r u - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))
⊢ v (step u) = Prod.swap (v u)
[PROOFSTEP]
ext
[GOAL]
case h₁
u : XgcdType
hr✝ : r u ≠ 0
ha : r u + ↑(b u) * q u = ↑(a u) := rq_eq u
hr : r u - 1 + 1 = r u := Eq.trans (add_comm (r u - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))
⊢ (v (step u)).fst = (Prod.swap (v u)).fst
[PROOFSTEP]
change ((u.y * u.q + u.z) * u.b + u.y * (u.r - 1 + 1) : ℕ) = u.y * u.a + u.z * u.b
[GOAL]
case h₁
u : XgcdType
hr✝ : r u ≠ 0
ha : r u + ↑(b u) * q u = ↑(a u) := rq_eq u
hr : r u - 1 + 1 = r u := Eq.trans (add_comm (r u - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))
⊢ (u.y * q u + ↑(z u)) * ↑(b u) + u.y * (r u - 1 + 1) = u.y * ↑(a u) + ↑(z u) * ↑(b u)
[PROOFSTEP]
rw [← ha, hr]
[GOAL]
case h₁
u : XgcdType
hr✝ : r u ≠ 0
ha : r u + ↑(b u) * q u = ↑(a u) := rq_eq u
hr : r u - 1 + 1 = r u := Eq.trans (add_comm (r u - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))
⊢ (u.y * q u + ↑(z u)) * ↑(b u) + u.y * r u = u.y * (r u + ↑(b u) * q u) + ↑(z u) * ↑(b u)
[PROOFSTEP]
ring
[GOAL]
case h₂
u : XgcdType
hr✝ : r u ≠ 0
ha : r u + ↑(b u) * q u = ↑(a u) := rq_eq u
hr : r u - 1 + 1 = r u := Eq.trans (add_comm (r u - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))
⊢ (v (step u)).snd = (Prod.swap (v u)).snd
[PROOFSTEP]
change ((u.w * u.q + u.x) * u.b + u.w * (u.r - 1 + 1) : ℕ) = u.w * u.a + u.x * u.b
[GOAL]
case h₂
u : XgcdType
hr✝ : r u ≠ 0
ha : r u + ↑(b u) * q u = ↑(a u) := rq_eq u
hr : r u - 1 + 1 = r u := Eq.trans (add_comm (r u - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))
⊢ (↑(w u) * q u + u.x) * ↑(b u) + ↑(w u) * (r u - 1 + 1) = ↑(w u) * ↑(a u) + u.x * ↑(b u)
[PROOFSTEP]
rw [← ha, hr]
[GOAL]
case h₂
u : XgcdType
hr✝ : r u ≠ 0
ha : r u + ↑(b u) * q u = ↑(a u) := rq_eq u
hr : r u - 1 + 1 = r u := Eq.trans (add_comm (r u - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))
⊢ (↑(w u) * q u + u.x) * ↑(b u) + ↑(w u) * r u = ↑(w u) * (r u + ↑(b u) * q u) + u.x * ↑(b u)
[PROOFSTEP]
ring
[GOAL]
u : XgcdType
_h : ¬r u = 0
⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 (step u) u
[PROOFSTEP]
apply u.step_wf _h
[GOAL]
u✝ u : XgcdType
h : r u = 0
⊢ reduce u = finish u
[PROOFSTEP]
rw [reduce]
[GOAL]
u✝ u : XgcdType
h : r u = 0
⊢ (if x : r u = 0 then finish u else flip (reduce (step u))) = finish u
[PROOFSTEP]
exact if_pos h
[GOAL]
u✝ u : XgcdType
h : r u ≠ 0
⊢ reduce u = flip (reduce (step u))
[PROOFSTEP]
rw [reduce]
[GOAL]
u✝ u : XgcdType
h : r u ≠ 0
⊢ (if x : r u = 0 then finish u else flip (reduce (step u))) = flip (reduce (step u))
[PROOFSTEP]
exact if_neg h
[GOAL]
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : r u = 0
⊢ IsReduced (reduce x✝)
[PROOFSTEP]
rw [reduce_a h]
[GOAL]
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : r u = 0
⊢ IsReduced (finish u)
[PROOFSTEP]
exact u.finish_isReduced
[GOAL]
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : ¬r u = 0
⊢ IsReduced (reduce x✝)
[PROOFSTEP]
have : SizeOf.sizeOf u.step < SizeOf.sizeOf u := u.step_wf h
[GOAL]
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : ¬r u = 0
this : sizeOf (step u) < sizeOf u
⊢ IsReduced (reduce x✝)
[PROOFSTEP]
rw [reduce_b h, flip_isReduced]
[GOAL]
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : ¬r u = 0
this : sizeOf (step u) < sizeOf u
⊢ IsReduced (reduce (step u))
[PROOFSTEP]
apply reduce_isReduced
[GOAL]
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : r u = 0
hs : IsSpecial x✝
⊢ IsSpecial (reduce x✝)
[PROOFSTEP]
rw [reduce_a h]
[GOAL]
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : r u = 0
hs : IsSpecial x✝
⊢ IsSpecial (finish u)
[PROOFSTEP]
exact u.finish_isSpecial hs
[GOAL]
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : ¬r u = 0
hs : IsSpecial x✝
⊢ IsSpecial (reduce x✝)
[PROOFSTEP]
have : SizeOf.sizeOf u.step < SizeOf.sizeOf u := u.step_wf h
[GOAL]
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : ¬r u = 0
hs : IsSpecial x✝
this : sizeOf (step u) < sizeOf u
⊢ IsSpecial (reduce x✝)
[PROOFSTEP]
rw [reduce_b h]
[GOAL]
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : ¬r u = 0
hs : IsSpecial x✝
this : sizeOf (step u) < sizeOf u
⊢ IsSpecial (flip (reduce (step u)))
[PROOFSTEP]
exact (flip_isSpecial _).mpr (reduce_isSpecial _ (u.step_isSpecial hs))
[GOAL]
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : r u = 0
⊢ v (reduce x✝) = v x✝
[PROOFSTEP]
rw [reduce_a h, finish_v u h]
[GOAL]
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : ¬r u = 0
⊢ v (reduce x✝) = v x✝
[PROOFSTEP]
have : SizeOf.sizeOf u.step < SizeOf.sizeOf u := u.step_wf h
[GOAL]
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : ¬r u = 0
this : sizeOf (step u) < sizeOf u
⊢ v (reduce x✝) = v x✝
[PROOFSTEP]
rw [reduce_b h, flip_v, reduce_v (step u), step_v u h, Prod.swap_swap]
[GOAL]
a b : ℕ+
⊢ ↑(gcdA' a b) = ↑(gcdW a b) + gcdX a b
[PROOFSTEP]
dsimp [gcdA', gcdX, gcdW, XgcdType.w]
[GOAL]
a b : ℕ+
⊢ succ ((xgcd a b).wp + (xgcd a b).x) = succ (xgcd a b).wp + (xgcd a b).x
[PROOFSTEP]
rw [Nat.succ_eq_add_one, Nat.succ_eq_add_one, add_right_comm]
[GOAL]
a b : ℕ+
⊢ ↑(gcdB' a b) = gcdY a b + ↑(gcdZ a b)
[PROOFSTEP]
dsimp [gcdB', gcdY, gcdZ, XgcdType.z]
[GOAL]
a b : ℕ+
⊢ succ ((xgcd a b).y + (xgcd a b).zp) = (xgcd a b).y + succ (xgcd a b).zp
[PROOFSTEP]
rw [Nat.succ_eq_add_one, Nat.succ_eq_add_one, add_assoc]
[GOAL]
a b : ℕ+
⊢ let d := gcdD a b;
  let w := gcdW a b;
  let x := gcdX a b;
  let y := gcdY a b;
  let z := gcdZ a b;
  let a' := gcdA' a b;
  let b' := gcdB' a b;
  w * z = succPNat (x * y) ∧
    a = a' * d ∧
      b = b' * d ∧
        z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
intros d w x y z a' b'
[GOAL]
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
⊢ w * z = succPNat (x * y) ∧
    a = a' * d ∧
      b = b' * d ∧
        z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
let u := XgcdType.start a b
[GOAL]
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
⊢ w * z = succPNat (x * y) ∧
    a = a' * d ∧
      b = b' * d ∧
        z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
let ur := u.reduce
[GOAL]
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
⊢ w * z = succPNat (x * y) ∧
    a = a' * d ∧
      b = b' * d ∧
        z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
have _ : d = ur.a := rfl
[GOAL]
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝ : d = XgcdType.a ur
⊢ w * z = succPNat (x * y) ∧
    a = a' * d ∧
      b = b' * d ∧
        z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
have hb : d = ur.b := u.reduce_isReduced'
[GOAL]
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝ : d = XgcdType.a ur
hb : d = XgcdType.b ur
⊢ w * z = succPNat (x * y) ∧
    a = a' * d ∧
      b = b' * d ∧
        z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
have ha' : (a' : ℕ) = w + x := gcdA'_coe a b
[GOAL]
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
⊢ w * z = succPNat (x * y) ∧
    a = a' * d ∧
      b = b' * d ∧
        z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
have hb' : (b' : ℕ) = y + z := gcdB'_coe a b
[GOAL]
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
⊢ w * z = succPNat (x * y) ∧
    a = a' * d ∧
      b = b' * d ∧
        z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
have hdet : w * z = succPNat (x * y) := u.reduce_isSpecial' rfl
[GOAL]
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
⊢ w * z = succPNat (x * y) ∧
    a = a' * d ∧
      b = b' * d ∧
        z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
constructor
[GOAL]
case left
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
⊢ w * z = succPNat (x * y)
case right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
⊢ a = a' * d ∧
    b = b' * d ∧
      z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
exact hdet
[GOAL]
case right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
⊢ a = a' * d ∧
    b = b' * d ∧
      z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
have hdet' : (w * z : ℕ) = x * y + 1 := by rw [← mul_coe, hdet, succPNat_coe]
[GOAL]
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
⊢ ↑w * ↑z = x * y + 1
[PROOFSTEP]
rw [← mul_coe, hdet, succPNat_coe]
[GOAL]
case right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
⊢ a = a' * d ∧
    b = b' * d ∧
      z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
have _ : u.v = ⟨a, b⟩ := XgcdType.start_v a b
[GOAL]
case right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
⊢ a = a' * d ∧
    b = b' * d ∧
      z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
let hv : Prod.mk (w * d + x * ur.b : ℕ) (y * d + z * ur.b : ℕ) = ⟨a, b⟩ := u.reduce_v.trans (XgcdType.start_v a b)
[GOAL]
case right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑w * ↑d + x * ↑(XgcdType.b ur), y * ↑d + ↑z * ↑(XgcdType.b ur)) = (↑a, ↑b) :=
  Eq.trans (XgcdType.reduce_v u) (XgcdType.start_v a b)
⊢ a = a' * d ∧
    b = b' * d ∧
      z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
rw [← hb, ← add_mul, ← add_mul, ← ha', ← hb'] at hv 
[GOAL]
case right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
⊢ a = a' * d ∧
    b = b' * d ∧
      z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
have ha'' : (a : ℕ) = a' * d := (congr_arg Prod.fst hv).symm
[GOAL]
case right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
⊢ a = a' * d ∧
    b = b' * d ∧
      z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
have hb'' : (b : ℕ) = b' * d := (congr_arg Prod.snd hv).symm
[GOAL]
case right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
⊢ a = a' * d ∧
    b = b' * d ∧
      z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
constructor
[GOAL]
case right.left
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
⊢ a = a' * d
case right.right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
⊢ b = b' * d ∧ z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
exact eq ha''
[GOAL]
case right.right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
⊢ b = b' * d ∧ z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
constructor
[GOAL]
case right.right.left
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
⊢ b = b' * d
case right.right.right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
⊢ z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
exact eq hb''
[GOAL]
case right.right.right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
⊢ z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
have hza' : (z * a' : ℕ) = x * b' + 1 :=
  by
  rw [ha', hb', mul_add, mul_add, mul_comm (z : ℕ), hdet']
  ring
[GOAL]
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
⊢ ↑z * ↑a' = x * ↑b' + 1
[PROOFSTEP]
rw [ha', hb', mul_add, mul_add, mul_comm (z : ℕ), hdet']
[GOAL]
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
⊢ x * y + 1 + ↑z * x = x * y + x * ↑z + 1
[PROOFSTEP]
ring
[GOAL]
case right.right.right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
⊢ z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
have hwb' : (w * b' : ℕ) = y * a' + 1 :=
  by
  rw [ha', hb', mul_add, mul_add, hdet']
  ring
[GOAL]
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
⊢ ↑w * ↑b' = y * ↑a' + 1
[PROOFSTEP]
rw [ha', hb', mul_add, mul_add, hdet']
[GOAL]
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
⊢ ↑w * y + (x * y + 1) = y * ↑w + y * x + 1
[PROOFSTEP]
ring
[GOAL]
case right.right.right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
constructor
[GOAL]
case right.right.right.left
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ z * a' = succPNat (x * ↑b')
[PROOFSTEP]
apply eq
[GOAL]
case right.right.right.left.a
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ ↑(z * a') = ↑(succPNat (x * ↑b'))
[PROOFSTEP]
rw [succPNat_coe, Nat.succ_eq_add_one, mul_coe, hza']
[GOAL]
case right.right.right.right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
constructor
[GOAL]
case right.right.right.right.left
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ w * b' = succPNat (y * ↑a')
[PROOFSTEP]
apply eq
[GOAL]
case right.right.right.right.left.a
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ ↑(w * b') = ↑(succPNat (y * ↑a'))
[PROOFSTEP]
rw [succPNat_coe, Nat.succ_eq_add_one, mul_coe, hwb']
[GOAL]
case right.right.right.right.right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
rw [ha'', hb'']
[GOAL]
case right.right.right.right.right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ ↑z * (↑a' * ↑d) = x * (↑b' * ↑d) + ↑d ∧ ↑w * (↑b' * ↑d) = y * (↑a' * ↑d) + ↑d
[PROOFSTEP]
repeat' rw [← @mul_assoc]
[GOAL]
case right.right.right.right.right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ ↑z * (↑a' * ↑d) = x * (↑b' * ↑d) + ↑d ∧ ↑w * (↑b' * ↑d) = y * (↑a' * ↑d) + ↑d
[PROOFSTEP]
rw [← @mul_assoc]
[GOAL]
case right.right.right.right.right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ ↑z * ↑a' * ↑d = x * (↑b' * ↑d) + ↑d ∧ ↑w * (↑b' * ↑d) = y * (↑a' * ↑d) + ↑d
[PROOFSTEP]
rw [← @mul_assoc]
[GOAL]
case right.right.right.right.right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ ↑z * ↑a' * ↑d = x * ↑b' * ↑d + ↑d ∧ ↑w * (↑b' * ↑d) = y * (↑a' * ↑d) + ↑d
[PROOFSTEP]
rw [← @mul_assoc]
[GOAL]
case right.right.right.right.right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ ↑z * ↑a' * ↑d = x * ↑b' * ↑d + ↑d ∧ ↑w * ↑b' * ↑d = y * (↑a' * ↑d) + ↑d
[PROOFSTEP]
rw [← @mul_assoc]
[GOAL]
case right.right.right.right.right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ ↑z * ↑a' * ↑d = x * ↑b' * ↑d + ↑d ∧ ↑w * ↑b' * ↑d = y * ↑a' * ↑d + ↑d
[PROOFSTEP]
rw [← @mul_assoc]
[GOAL]
case right.right.right.right.right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ ↑z * ↑a' * ↑d = x * ↑b' * ↑d + ↑d ∧ ↑w * ↑b' * ↑d = y * ↑a' * ↑d + ↑d
[PROOFSTEP]
rw [hza', hwb']
[GOAL]
case right.right.right.right.right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ (x * ↑b' + 1) * ↑d = x * ↑b' * ↑d + ↑d ∧ (y * ↑a' + 1) * ↑d = y * ↑a' * ↑d + ↑d
[PROOFSTEP]
constructor
[GOAL]
case right.right.right.right.right.left
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ (x * ↑b' + 1) * ↑d = x * ↑b' * ↑d + ↑d
[PROOFSTEP]
ring
[GOAL]
case right.right.right.right.right.right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ (y * ↑a' + 1) * ↑d = y * ↑a' * ↑d + ↑d
[PROOFSTEP]
ring
[GOAL]
a b : ℕ+
⊢ gcdD a b = gcd a b
[PROOFSTEP]
rcases gcd_props a b with ⟨_, h₁, h₂, _, _, h₅, _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
a b : ℕ+
left✝² : gcdW a b * gcdZ a b = succPNat (gcdX a b * gcdY a b)
h₁ : a = gcdA' a b * gcdD a b
h₂ : b = gcdB' a b * gcdD a b
left✝¹ : gcdZ a b * gcdA' a b = succPNat (gcdX a b * ↑(gcdB' a b))
left✝ : gcdW a b * gcdB' a b = succPNat (gcdY a b * ↑(gcdA' a b))
h₅ : ↑(gcdZ a b) * ↑a = gcdX a b * ↑b + ↑(gcdD a b)
right✝ : ↑(gcdW a b) * ↑b = gcdY a b * ↑a + ↑(gcdD a b)
⊢ gcdD a b = gcd a b
[PROOFSTEP]
apply dvd_antisymm
[GOAL]
case intro.intro.intro.intro.intro.intro.a
a b : ℕ+
left✝² : gcdW a b * gcdZ a b = succPNat (gcdX a b * gcdY a b)
h₁ : a = gcdA' a b * gcdD a b
h₂ : b = gcdB' a b * gcdD a b
left✝¹ : gcdZ a b * gcdA' a b = succPNat (gcdX a b * ↑(gcdB' a b))
left✝ : gcdW a b * gcdB' a b = succPNat (gcdY a b * ↑(gcdA' a b))
h₅ : ↑(gcdZ a b) * ↑a = gcdX a b * ↑b + ↑(gcdD a b)
right✝ : ↑(gcdW a b) * ↑b = gcdY a b * ↑a + ↑(gcdD a b)
⊢ gcdD a b ∣ gcd a b
[PROOFSTEP]
apply dvd_gcd
[GOAL]
case intro.intro.intro.intro.intro.intro.a.hm
a b : ℕ+
left✝² : gcdW a b * gcdZ a b = succPNat (gcdX a b * gcdY a b)
h₁ : a = gcdA' a b * gcdD a b
h₂ : b = gcdB' a b * gcdD a b
left✝¹ : gcdZ a b * gcdA' a b = succPNat (gcdX a b * ↑(gcdB' a b))
left✝ : gcdW a b * gcdB' a b = succPNat (gcdY a b * ↑(gcdA' a b))
h₅ : ↑(gcdZ a b) * ↑a = gcdX a b * ↑b + ↑(gcdD a b)
right✝ : ↑(gcdW a b) * ↑b = gcdY a b * ↑a + ↑(gcdD a b)
⊢ gcdD a b ∣ a
case intro.intro.intro.intro.intro.intro.a.hn
a b : ℕ+
left✝² : gcdW a b * gcdZ a b = succPNat (gcdX a b * gcdY a b)
h₁ : a = gcdA' a b * gcdD a b
h₂ : b = gcdB' a b * gcdD a b
left✝¹ : gcdZ a b * gcdA' a b = succPNat (gcdX a b * ↑(gcdB' a b))
left✝ : gcdW a b * gcdB' a b = succPNat (gcdY a b * ↑(gcdA' a b))
h₅ : ↑(gcdZ a b) * ↑a = gcdX a b * ↑b + ↑(gcdD a b)
right✝ : ↑(gcdW a b) * ↑b = gcdY a b * ↑a + ↑(gcdD a b)
⊢ gcdD a b ∣ b
[PROOFSTEP]
exact Dvd.intro (gcdA' a b) (h₁.trans (mul_comm _ _)).symm
[GOAL]
case intro.intro.intro.intro.intro.intro.a.hn
a b : ℕ+
left✝² : gcdW a b * gcdZ a b = succPNat (gcdX a b * gcdY a b)
h₁ : a = gcdA' a b * gcdD a b
h₂ : b = gcdB' a b * gcdD a b
left✝¹ : gcdZ a b * gcdA' a b = succPNat (gcdX a b * ↑(gcdB' a b))
left✝ : gcdW a b * gcdB' a b = succPNat (gcdY a b * ↑(gcdA' a b))
h₅ : ↑(gcdZ a b) * ↑a = gcdX a b * ↑b + ↑(gcdD a b)
right✝ : ↑(gcdW a b) * ↑b = gcdY a b * ↑a + ↑(gcdD a b)
⊢ gcdD a b ∣ b
[PROOFSTEP]
exact Dvd.intro (gcdB' a b) (h₂.trans (mul_comm _ _)).symm
[GOAL]
case intro.intro.intro.intro.intro.intro.a
a b : ℕ+
left✝² : gcdW a b * gcdZ a b = succPNat (gcdX a b * gcdY a b)
h₁ : a = gcdA' a b * gcdD a b
h₂ : b = gcdB' a b * gcdD a b
left✝¹ : gcdZ a b * gcdA' a b = succPNat (gcdX a b * ↑(gcdB' a b))
left✝ : gcdW a b * gcdB' a b = succPNat (gcdY a b * ↑(gcdA' a b))
h₅ : ↑(gcdZ a b) * ↑a = gcdX a b * ↑b + ↑(gcdD a b)
right✝ : ↑(gcdW a b) * ↑b = gcdY a b * ↑a + ↑(gcdD a b)
⊢ gcd a b ∣ gcdD a b
[PROOFSTEP]
have h₇ : (gcd a b : ℕ) ∣ gcdZ a b * a := (Nat.gcd_dvd_left a b).trans (dvd_mul_left _ _)
[GOAL]
case intro.intro.intro.intro.intro.intro.a
a b : ℕ+
left✝² : gcdW a b * gcdZ a b = succPNat (gcdX a b * gcdY a b)
h₁ : a = gcdA' a b * gcdD a b
h₂ : b = gcdB' a b * gcdD a b
left✝¹ : gcdZ a b * gcdA' a b = succPNat (gcdX a b * ↑(gcdB' a b))
left✝ : gcdW a b * gcdB' a b = succPNat (gcdY a b * ↑(gcdA' a b))
h₅ : ↑(gcdZ a b) * ↑a = gcdX a b * ↑b + ↑(gcdD a b)
right✝ : ↑(gcdW a b) * ↑b = gcdY a b * ↑a + ↑(gcdD a b)
h₇ : ↑(gcd a b) ∣ ↑(gcdZ a b) * ↑a
⊢ gcd a b ∣ gcdD a b
[PROOFSTEP]
have h₈ : (gcd a b : ℕ) ∣ gcdX a b * b := (Nat.gcd_dvd_right a b).trans (dvd_mul_left _ _)
[GOAL]
case intro.intro.intro.intro.intro.intro.a
a b : ℕ+
left✝² : gcdW a b * gcdZ a b = succPNat (gcdX a b * gcdY a b)
h₁ : a = gcdA' a b * gcdD a b
h₂ : b = gcdB' a b * gcdD a b
left✝¹ : gcdZ a b * gcdA' a b = succPNat (gcdX a b * ↑(gcdB' a b))
left✝ : gcdW a b * gcdB' a b = succPNat (gcdY a b * ↑(gcdA' a b))
h₅ : ↑(gcdZ a b) * ↑a = gcdX a b * ↑b + ↑(gcdD a b)
right✝ : ↑(gcdW a b) * ↑b = gcdY a b * ↑a + ↑(gcdD a b)
h₇ : ↑(gcd a b) ∣ ↑(gcdZ a b) * ↑a
h₈ : ↑(gcd a b) ∣ gcdX a b * ↑b
⊢ gcd a b ∣ gcdD a b
[PROOFSTEP]
rw [h₅] at h₇ 
[GOAL]
case intro.intro.intro.intro.intro.intro.a
a b : ℕ+
left✝² : gcdW a b * gcdZ a b = succPNat (gcdX a b * gcdY a b)
h₁ : a = gcdA' a b * gcdD a b
h₂ : b = gcdB' a b * gcdD a b
left✝¹ : gcdZ a b * gcdA' a b = succPNat (gcdX a b * ↑(gcdB' a b))
left✝ : gcdW a b * gcdB' a b = succPNat (gcdY a b * ↑(gcdA' a b))
h₅ : ↑(gcdZ a b) * ↑a = gcdX a b * ↑b + ↑(gcdD a b)
right✝ : ↑(gcdW a b) * ↑b = gcdY a b * ↑a + ↑(gcdD a b)
h₇ : ↑(gcd a b) ∣ gcdX a b * ↑b + ↑(gcdD a b)
h₈ : ↑(gcd a b) ∣ gcdX a b * ↑b
⊢ gcd a b ∣ gcdD a b
[PROOFSTEP]
rw [dvd_iff]
[GOAL]
case intro.intro.intro.intro.intro.intro.a
a b : ℕ+
left✝² : gcdW a b * gcdZ a b = succPNat (gcdX a b * gcdY a b)
h₁ : a = gcdA' a b * gcdD a b
h₂ : b = gcdB' a b * gcdD a b
left✝¹ : gcdZ a b * gcdA' a b = succPNat (gcdX a b * ↑(gcdB' a b))
left✝ : gcdW a b * gcdB' a b = succPNat (gcdY a b * ↑(gcdA' a b))
h₅ : ↑(gcdZ a b) * ↑a = gcdX a b * ↑b + ↑(gcdD a b)
right✝ : ↑(gcdW a b) * ↑b = gcdY a b * ↑a + ↑(gcdD a b)
h₇ : ↑(gcd a b) ∣ gcdX a b * ↑b + ↑(gcdD a b)
h₈ : ↑(gcd a b) ∣ gcdX a b * ↑b
⊢ ↑(gcd a b) ∣ ↑(gcdD a b)
[PROOFSTEP]
exact (Nat.dvd_add_iff_right h₈).mpr h₇
