proposition: Lemma tool_undup_size : forall (l l': seq T), size (undup l') <= size (undup (l++l')).
proof: Proof. elim => [ | hd tl hi] l' //=. case: (hd \in tl ++ l') => //=. by apply (@leq_trans (size (undup (tl++l')))). Qed.
imports: Coq(Mergesort Permutation) HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(path)