theorem HexBerlekampZassenhausMathlib.BHKS.supportPartitionByMinColumn_length_eq_ncard_of_partition {r : ℕ} (trueSupports : Set (Set (Fin r))) (hcover : ∀ (i : Fin r), ∃ S ∈ trueSupports, i ∈ S) (hdisj : ∀ S ∈ trueSupports, ∀ T ∈ trueSupports, ∀ i ∈ S, i ∈ T → S = T) (hne : ∀ S ∈ trueSupports, S.Nonempty) : (supportPartitionByMinColumn trueSupports).length = trueSupports.ncard

For a partition trueSupports, the support-equivalence partition has exactly one class per part: its length equals the number of parts trueSupports.ncard.