proposition: Lemma tool_undup_size2 : forall (l l': seq T), size (undup l) <= size (undup (l++l')).
proof: Proof. move => l l'. rewrite (@perm_size _ (undup (l ++ l')) (undup (l'++l))). by apply tool_undup_size. apply uniq_perm. by apply undup_uniq. by apply undup_uniq. move => u. rewrite !mem_undup !mem_cat. by apply orbC. Qed.
imports: Coq(Mergesort Permutation) HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(path)