rw [← tsub_pos_iff_lt, ← card_sdiff (mul_subset_mul hs ht), card_pos]
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hC : C.Nonempty
hs : s' ⊆ s
ht : t' ⊆ t
hCst : C ⊆ s * t
hCst' : Disjoint C (s' * t')
⊢ (s' * t').card < (s * t).card
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s s' t t' C : Finset α
a b : α
hC : C.Nonempty
hs : s' ⊆ s
ht : t' ⊆ t
hCst : C ⊆ s * t
hCst' : Disjoint C (s' * t')
⊢ ((s * t) \ (s' * t')).Nonempty