proposition: Lemma exists_has (T : finType) (p : {pred T}) : [exists x, p x] = has p (enum T).
proof: Proof. by rewrite -[LHS]negbK negb_exists forall_all all_predC negbK. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)