proposition: Lemma list_to_setK m l: size l = m -> char_seq (list_to_set m l) = l.
proof: Proof. move => ss. apply: (eq_from_nth (x0:=false)); rewrite size_char_seq => // i lim. by rewrite char_seq_prop inE. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)