proposition: Lemma card_intcompn : #|{:intcompn}| = 2 ^ n.-1.
proof: Proof. rewrite /= !cardT -!(size_map val) !enumT. rewrite unlock !subType_seqP ?enum_compn_allP //=. elim/ltn_ind: n => [[_ | i IHi]] /=; first by rewrite expn0. rewrite enum_compnE // size_allpairs_dep sumn_mapE. rewrite -{1}(subn0 i.+1) -subSS -/(index_iota _ _) big_add1 /= big_mkord. transitivity (\sum_(k < i.+1) 2 ^ k.-1). rewrite (reindex_inj rev_ord_inj) /=; apply eq_bigr => k _. by rewrite !subSS subKn ?IHi // -ltnS. rewrite big_ord_recl //= expn0 -(mul1n (\sum__ _)) -(predn_exp 2 i). by rewrite add1n prednK // expn_gt0. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted partition subseq ordtype