linarith [ih]
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hdisj : Disjoint C (s' * t')
H : Finset α := C.mulStab
H' : Finset α := (s' * t').mulStab
hsub : H' ⊆ H
C' : Finset α := C ∪ s' * t'
hCun : C'.mulStab = H'
hconv : ↑(s ∩ t).card + ↑((s ∪ t) * H).card ≤ ↑C.card + ↑H.card
hnotconv : ↑C'.card + ↑C'.mulStab.card < ↑(s ∩ t).card + ↑((s ∪ t) * C'.mulStab).card
ih : ↑(s' * H').card + ↑(t' * H').card ≤ ↑(s' * t').card + ↑H'.card
⊢ ↑H.card - ↑(s' * t').card - ↑H'.card ≤ ↑H.card - ↑(s' * H').card - ↑(t' * H').card
no goals