induction n using Nat.prime_composite_induction
n p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
s : Multiset (ZMod n)
hs : 2 * n - 1 ≤ Multiset.card s
⊢ ∃ t ≤ s, Multiset.card t = n ∧ t.sum = 0
case 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

case one
n p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
s : Multiset (ZMod 1)
hs : 2 * 1 - 1 ≤ Multiset.card s
⊢ ∃ t ≤ s, Multiset.card t = 1 ∧ t.sum = 0

case prime
n p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
p✝ : ℕ
a✝ : p✝.Prime
s : Multiset (ZMod p✝)
hs : 2 * p✝ - 1 ≤ Multiset.card s
⊢ ∃ t ≤ s, Multiset.card t = p✝ ∧ t.sum = 0

case composite
n p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
a✝⁴ : ℕ
a✝³ : 2 ≤ a✝⁴
a✝² : ∀ {s : Multiset (ZMod a✝⁴)}, 2 * a✝⁴ - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = a✝⁴ ∧ t.sum = 0
b✝ : ℕ
a✝¹ : 2 ≤ b✝
a✝ : ∀ {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
⊢ ∃ t ≤ s, Multiset.card t = a✝⁴ * b✝ ∧ t.sum = 0