proposition: Lemma set_to_list_cardinal m (X: {set 'I_m}) : #|X| = DP_Tcount (char_seq X).
proof: Proof. rewrite /DP_Tcount/char_seq -sum1_count big_mkcond big_map -big_mkcond. rewrite -sum1_card -big_enum big_filter big_filter_cond. by apply: eq_big => // i /=; case: (i \in X). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)