proposition: Lemma undup_flatten_nseq n (T : eqType) (s : seq T) : 0 < n -> undup (flatten (nseq n s)) = undup s.
proof: Proof. elim: n => [|[|n]/= IHn]//= _; rewrite ?cats0// undup_cat {}IHn//. rewrite (@eq_in_filter _ _ pred0) ?filter_pred0// => x. by rewrite mem_undup mem_cat => ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)