Face and corner matching for targets in tableau row 0

theorem MacMahon.face_corner_01 (p : Pair) (k : Slot) : HasCorner p (cornerAt 0 1 k) ↔ ∃ (r : Fin 24), FaceFits (0, 1) p k r

theorem MacMahon.face_corner_02 (p : Pair) (k : Slot) : HasCorner p (cornerAt 0 2 k) ↔ ∃ (r : Fin 24), FaceFits (0, 2) p k r

theorem MacMahon.face_corner_03 (p : Pair) (k : Slot) : HasCorner p (cornerAt 0 3 k) ↔ ∃ (r : Fin 24), FaceFits (0, 3) p k r

theorem MacMahon.face_corner_04 (p : Pair) (k : Slot) : HasCorner p (cornerAt 0 4 k) ↔ ∃ (r : Fin 24), FaceFits (0, 4) p k r

theorem MacMahon.face_corner_05 (p : Pair) (k : Slot) : HasCorner p (cornerAt 0 5 k) ↔ ∃ (r : Fin 24), FaceFits (0, 5) p k r