proposition: Lemma mem_catD (T:finType) (x:T) (s1 s2 : seq T) : [disjoint s1 & s2] -> (x \in s1 ++ s2) = (x \in s1) (+) (x \in s2).
proof: Proof. move => D. rewrite mem_cat. case C1 : (x \in s1) => //=. symmetry. apply/negP. exact: disjointE D _. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)