no goals
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : r u = 0
⊢ v (reduce x✝) = v x✝
rw [reduce_a h, finish_v u h]
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : ¬r u = 0
this : sizeOf (step u) < sizeOf u
⊢ v (reduce x✝) = v x✝
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : ¬r u = 0
⊢ v (reduce x✝) = v x✝
have : SizeOf.sizeOf u.step < SizeOf.sizeOf u := u.step_wf h
no goals
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : ¬r u = 0
this : sizeOf (step u) < sizeOf u
⊢ v (reduce x✝) = v x✝
rw [reduce_b h, flip_v, reduce_v (step u), step_v u h, Prod.swap_swap]