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