u✝ x✝ : XgcdType
u : XgcdType := x✝
h : r u = 0
⊢ IsReduced (finish u)
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : r u = 0
⊢ IsReduced (reduce x✝)
rw [reduce_a h]
no goals
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : r u = 0
⊢ IsReduced (finish u)
exact u.finish_isReduced
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : ¬r u = 0
this : sizeOf (step u) < sizeOf u
⊢ IsReduced (reduce x✝)
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : ¬r u = 0
⊢ IsReduced (reduce x✝)
have : SizeOf.sizeOf u.step < SizeOf.sizeOf u := u.step_wf h
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : ¬r u = 0
this : sizeOf (step u) < sizeOf u
⊢ IsReduced (reduce (step u))
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : ¬r u = 0
this : sizeOf (step u) < sizeOf u
⊢ IsReduced (reduce x✝)
rw [reduce_b h, flip_isReduced]
no goals
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : ¬r u = 0
this : sizeOf (step u) < sizeOf u
⊢ IsReduced (reduce (step u))
apply reduce_isReduced