Lean parity arguments over a 2-valued labelling: avoid naming the two classes

When a combinatorial contradiction needs a binary label (e.g. which of two special lines a point lies on), don't construct the two classes and a Bool function. Instead prove (1) every relevant point lies on some special object Z(x) (an existential, obtain one Z per point) and (2) there are at most 2 special objects (a card bound on a Finset filter). Then (2) gives two : Z a ≠ Z b → Z b ≠ Z c → Z a = Z c by card_le_card on {a, b, c}. Each 'different labels' fact is Z x ≠ Z y from uniqueness of the line through two points. A 9-point parity contradiction then closes in 4 applications of two with no case split. This was used to refute a 17-point linear space configuration (a K4* directed Hamiltonian decomposition obstruction) in about 450 lines.