proposition: Lemma cat_uniq s1 s2 : uniq (s1 ++ s2) = [&& uniq s1, ~~ has (mem s1) s2 & uniq s2].
proof: Proof. elim: s1 => [| x s1 ihs1] /=; first by rewrite has_pred0 //. rewrite mem_cat negb_or. rewrite has_sym. rewrite /= negb_or. rewrite -!andbA. do !bool_congr. rewrite has_sym. done. Qed.
imports: Coq(ZArith) Arith Ring Coq(ssreflect) mathcomp(ssrfun ssrbool) mathcomp(all_ssreflect)