proposition: Lemma char_seq_prop m (X: {set 'I_m}) k (km: k < m): nth false (char_seq X) k = ((Ordinal km) \in X).
proof: Proof. have km1: k < size (enum 'I_m) by rewrite (size_enum_ord m). set K := (Ordinal km). by rewrite/char_seq (nth_map K false _ km1) (nth_ord_enum K K). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)