proposition: Lemma uniq_catRL (T : eqType) (x : T) s1 s2 : uniq (s1 ++ s2) -> x \in s1 ++ s2 -> uniq (s1 ++ s2) -> (x \in s2) = (x \notin s1).
proof: Proof. rewrite mem_cat uniq_catC => s_uniq x_s. by rewrite (uniq_catLR s_uniq) // mem_cat orbC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple) mathcomp(bigop finset finfun perm fingraph path div) bigmin