proposition: Lemma card_isO n t : #|isO n t| = minn n t.
proof: Proof. apply/sym_equal. case: (leqP n t) => [nLt|tLn]. by rewrite isOE_ge //= cardsT card_ord. case: n tLn => // n tLn. rewrite isOE_le // card_imset // => [|i j /val_eqP/eqP /=]. by rewrite card_ord. by rewrite !inordK ?(leq_trans _ tLn) ?ltnS 1?ltnW // => /eqP/val_eqP. Qed.
imports: mathcomp(all_ssreflect finmap)