proposition: Lemma leq_cards_ord n (s : {set 'I_n}) : (#|s| <= n)%nat.
proof: Proof. by move/subset_leq_card: (subsetT s); rewrite cardsT card_ord. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist