proposition: Lemma uniq_catLR (T : eqType) (x : T) s1 s2 : uniq (s1 ++ s2) -> x \in s1 ++ s2 -> (x \in s1) = (x \notin s2).
proof: Proof. rewrite mem_cat=> s_uniq /orP[] x_in; move: s_uniq. by rewrite uniq_catC cat_uniq => /and3P[_ /hasPn /(_ _ x_in)->]. by rewrite cat_uniq => /and3P[_ /hasPn /(_ _ x_in) /= /negPf->]; rewrite x_in. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple) mathcomp(bigop finset finfun perm fingraph path div) bigmin