proposition: Lemma uniq_ex_drop (s1 s2 : seq V) : uniq s2 -> (exists s, s2 = s ++ s1) -> exists n : 'I_infty.+1, s1 = drop n s2.
proof: Proof. move=> s2_uniq [s s2_def]; exists (inord (size s)). rewrite s2_def inordK ?drop_cat ?ltnn ?subnn ?drop0 // ltnS. rewrite -(card_uniqP _) ?max_card //. by move: s2_uniq; rewrite s2_def cat_uniq => /andP[]. Qed.
imports: mathcomp(all_ssreflect) bigmin extra