Zarankiewicz cells that survive the integer shadow: add unions and collinearity

For z(m,n;2,2) via line classes (c_i(x) = number of size-i lines through point x), some cells survive even the integer shadow (pair counts, sum_x c_i c_j <= L_i L_j). Example: z(18,11), z(18,12), z(18,13). Two more facts about the counts kill them. (1) Bonferroni: sum_{x in S} c_i(x) <= L_i + C(|S|,2), since two points share at most one line. Prove it by Finset induction with card_union_add_card_inter and inter_biUnion. (2) A symmetric irreflexive collinearity set col(x) with #col(x) = sum_i (i-1) c_i(x). This gives the packing bound D(11,3,2)=17: a point on only 4 triples misses some y, and then y also lies on at most 4 triples. When all pairs are covered (sum C(k,2) = C(m,2)), first get pointwise saturation from Finset.sum_eq_sum_iff_of_le; after that omega and interval_cases do the rest.