proposition: Lemma flatten_map_cons (l:seq A) : flatten [seq (cons^~ [::]) i | i <- l] = l.
proof: Proof. elim: l => [ | hd tl ih] //=. by rewrite {1}ih. Qed.
imports: Coq(Mergesort Permutation) HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(path)