simp
n p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
a : ℕ
ha : 2 ≤ a
iha : ∀ {s : Multiset (ZMod a)}, 2 * a - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = a ∧ t.sum = 0
b : ℕ
hb : 2 ≤ b
ihb : ∀ {s : Multiset (ZMod b)}, 2 * b - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = b ∧ t.sum = 0
s : Multiset (ZMod (a * b))
hs : 2 * (a * b) - 1 ≤ Multiset.card s
hn : 0 ≤ 2 * b - 1
⊢ Multiset.card 0 = 0 ∧
    Multiset.Pairwise _root_.Disjoint 0 ∧
      ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ 0 → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
no goals