case zero => exact ⟨0, s.zero_le, card_zero, sum_zero⟩
n p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
s : Multiset (ZMod 0)
hs : 2 * 0 - 1 ≤ Multiset.card s
⊢ ∃ t ≤ s, Multiset.card t = 0 ∧ t.sum = 0
no goals