English
If P is equipartition, then the number of parts of size |s|/|P.parts| + 1 equals |s| mod |P.parts|.
Русский
Если P — равноправное разбиение, то число частей размера |s|/|P.parts| + 1 равно |s| мод |P.parts|.
LaTeX
$$#({p ∈ P.parts | #p = #s / #P.parts + 1}) = #s % #P.parts$$
Lean4
/-- An equipartition of a finset with `n` elements into `k` parts has
`n % k` parts of size `n / k + 1`. -/
theorem card_large_parts_eq_mod (hP : P.IsEquipartition) : #({p ∈ P.parts | #p = #s / #P.parts + 1}) = #s % #P.parts :=
by
have z := P.sum_card_parts
rw [← sum_filter_add_sum_filter_not (s := P.parts) (p := fun x ↦ #x = #s / #P.parts + 1),
hP.filter_ne_average_add_one_eq_average, sum_const_nat (m := #s / #P.parts + 1) (by simp),
sum_const_nat (m := #s / #P.parts) (by simp), ← hP.filter_ne_average_add_one_eq_average, mul_add, add_comm, ←
add_assoc, ← add_mul, mul_one, add_comm #_, filter_card_add_filter_neg_card_eq_card, add_comm] at z
rw [← add_left_inj, Nat.mod_add_div, z]
