case pos
u : XgcdType
hr : r u = 0
hq : q u = 0
⊢ q u = qp u + 1

case neg
u : XgcdType
hr : r u = 0
hq : ¬q u = 0
⊢ q u = qp u + 1
u : XgcdType
hr : r u = 0
⊢ q u = qp u + 1
by_cases hq : u.q = 0
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
case pos
u : XgcdType
hr : r u = 0
hq : q u = 0
⊢ q u = qp u + 1
let h := u.rq_eq
case pos
u : XgcdType
hr : r u = 0
hq : q u = 0
h : 0 = u.ap + 1
⊢ q u = qp u + 1
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
rw [hr, hq, mul_zero, add_zero] at h
no goals
case pos
u : XgcdType
hr : r u = 0
hq : q u = 0
h : 0 = u.ap + 1
⊢ q u = qp u + 1
cases h
no goals
case neg
u : XgcdType
hr : r u = 0
hq : ¬q u = 0
⊢ q u = qp u + 1
exact (Nat.succ_pred_eq_of_pos (Nat.pos_of_ne_zero hq)).symm