. exact BishopFin.card_subsingleton
case le
n i : Nat
h : i + 1 < n
⊢ BishopFin.card (Inversion (transposAdj i h)) ≤ 1

case ge
n i : Nat
h : i + 1 < n
⊢ 1 ≤ BishopFin.card (Inversion (transposAdj i h))
case ge
n i : Nat
h : i + 1 < n
⊢ 1 ≤ BishopFin.card (Inversion (transposAdj i h))