simpa [*] using add_kneser s t
case inl
p : ℕ
hp : p.Prime
s t : Finset (ZMod p)
hs : s.Nonempty
ht : t.Nonempty
this : Fact p.Prime
h : (s + t).addStab = 0
⊢ s.card + t.card - 1 ≤ (s + t).card
no goals