u : XgcdType
hr : r u ≠ 0
⊢ r u - 1 < u.bp
u : XgcdType
hr : r u ≠ 0
⊢ sizeOf (step u) < sizeOf u
change u.r - 1 < u.bp
u : XgcdType
hr : r u ≠ 0
h₀ : r u - 1 + 1 = r u
⊢ r u - 1 < u.bp
u : XgcdType
hr : r u ≠ 0
⊢ r u - 1 < u.bp
have h₀ : u.r - 1 + 1 = u.r := Nat.succ_pred_eq_of_pos (Nat.pos_of_ne_zero hr)
u : XgcdType
hr : r u ≠ 0
h₀ : r u - 1 + 1 = r u
h₁ : r u < u.bp + 1
⊢ r u - 1 < u.bp
u : XgcdType
hr : r u ≠ 0
h₀ : r u - 1 + 1 = r u
⊢ r u - 1 < u.bp
have h₁ : u.r < u.bp + 1 := Nat.mod_lt (u.ap + 1) u.bp.succ_pos
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
u : XgcdType
hr : r u ≠ 0
h₀ : r u - 1 + 1 = r u
h₁ : r u < u.bp + 1
⊢ r u - 1 < u.bp
rw [← h₀] at h₁
no goals
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
exact lt_of_succ_lt_succ h₁