proposition: Lemma take_find (T : Type) (a : pred T) s : ~~ has a (take (find a s) s).
proof: Proof. elim: s => //= x s IH. case E: (a x) => //=. by rewrite E. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)