proposition: Lemma undup_subseq s : subseq (undup s) s.
proof: Proof. elim: s => //= x s; case: (_ \in _); last by rewrite eqxx. by case: (undup s) => //= y u; case: (_ == _) => //=; apply: cons_subseq. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)