u✝ x✝ : XgcdType
u : XgcdType := x✝
h : r u = 0
hs : IsSpecial x✝
⊢ IsSpecial (finish u)
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : r u = 0
hs : IsSpecial x✝
⊢ IsSpecial (reduce x✝)
rw [reduce_a h]
no goals
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : r u = 0
hs : IsSpecial x✝
⊢ IsSpecial (finish u)
exact u.finish_isSpecial hs
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : ¬r u = 0
hs : IsSpecial x✝
this : sizeOf (step u) < sizeOf u
⊢ IsSpecial (reduce x✝)
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : ¬r u = 0
hs : IsSpecial x✝
⊢ IsSpecial (reduce x✝)
have : SizeOf.sizeOf u.step < SizeOf.sizeOf u := u.step_wf h
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : ¬r u = 0
hs : IsSpecial x✝
this : sizeOf (step u) < sizeOf u
⊢ IsSpecial (flip (reduce (step u)))
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : ¬r u = 0
hs : IsSpecial x✝
this : sizeOf (step u) < sizeOf u
⊢ IsSpecial (reduce x✝)
rw [reduce_b h]
no goals
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : ¬r u = 0
hs : IsSpecial x✝
this : sizeOf (step u) < sizeOf u
⊢ IsSpecial (flip (reduce (step u)))
exact (flip_isSpecial _).mpr (reduce_isSpecial _ (u.step_isSpecial hs))