proposition: Lemma disjointP (T : finType) (A B : pred T): reflect (forall x, x \in A -> x \in B -> False) [disjoint A & B].
proof: Proof. by rewrite disjoint_subset; apply:(iffP subsetP) => H x; move/H/negP. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)