u✝ u : XgcdType
h : r u = 0
⊢ (if x : r u = 0 then finish u else flip (reduce (step u))) = finish u
u✝ u : XgcdType
h : r u = 0
⊢ reduce u = finish u
rw [reduce]
no goals
u✝ u : XgcdType
h : r u = 0
⊢ (if x : r u = 0 then finish u else flip (reduce (step u))) = finish u
exact if_pos h