proposition: Lemma disjoints1 (T : finType) (A : {pred T}) x : [disjoint [set x] & A] = (x \notin A).
proof: Proof. by rewrite (@eq_disjoint1 _ x) // => y; rewrite !inE. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)