Corner incidence and usable varieties

theorem MacMahon.cornerAt_mem (i j : Label) : i ≠ j → ∀ (k : Slot), HasCorner (i, j) (cornerAt i j k)

theorem MacMahon.every_corner (c : Corner) : ∃ (i : Label) (j : Label), i ≠ j ∧ ∃ (k : Slot), cornerAt i j k = c

theorem MacMahon.usable_rule (i j : Label) : i ≠ j → ∀ (p : Pair), Usable (i, j) p ↔ p.1 ≠ p.2 ∧ (p = (i, j) ∨ p.1 ≠ i ∧ p.2 ≠ j ∧ p ≠ (j, i))

theorem MacMahon.partition_corner_support (b : Fin 10) (p : Pair) : HasCorner p (partitionCorner b) → winner b p = 1