u : XgcdType
a b : ℕ+
⊢ (succ 0 * succ (↑a - 1) + 0 * succ (↑b - 1), 0 * succ (↑a - 1) + succ 0 * succ (↑b - 1)) = (↑a, ↑b)
u : XgcdType
a b : ℕ+
⊢ v (start a b) = (↑a, ↑b)
dsimp [start, v, XgcdType.a, XgcdType.b, w, z]
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)
u : XgcdType
a b : ℕ+
⊢ (succ 0 * succ (↑a - 1) + 0 * succ (↑b - 1), 0 * succ (↑a - 1) + succ 0 * succ (↑b - 1)) = (↑a, ↑b)
have : succ 0 = 1 := rfl
u : XgcdType
a b : ℕ+
this : succ 0 = 1
⊢ (succ (↑a - 1), succ (↑b - 1)) = (↑a, ↑b)
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)
rw [this, one_mul, one_mul, zero_mul, zero_mul, zero_add, add_zero]
u : XgcdType
a b : ℕ+
this : succ 0 = 1
⊢ (succ (pred ↑a), succ (pred ↑b)) = (↑a, ↑b)
u : XgcdType
a b : ℕ+
this : succ 0 = 1
⊢ (succ (↑a - 1), succ (↑b - 1)) = (↑a, ↑b)
rw [← Nat.pred_eq_sub_one, ← Nat.pred_eq_sub_one]
no goals
u : XgcdType
a b : ℕ+
this : succ 0 = 1
⊢ (succ (pred ↑a), succ (pred ↑b)) = (↑a, ↑b)
rw [Nat.succ_pred_eq_of_pos a.pos, Nat.succ_pred_eq_of_pos b.pos]