refine' card_addStab_le_card.trans' _
case inr
p : ℕ
hp : p.Prime
s t : Finset (ZMod p)
hs : s.Nonempty
ht : t.Nonempty
this : Fact p.Prime
h : (s + t).addStab = univ
⊢ min p (s.card + t.card - 1) ≤ (s + t).card
case inr
p : ℕ
hp : p.Prime
s t : Finset (ZMod p)
hs : s.Nonempty
ht : t.Nonempty
this : Fact p.Prime
h : (s + t).addStab = univ
⊢ min p (s.card + t.card - 1) ≤ (s + t).addStab.card