proposition: Lemma fcard0P (T : finType) (A : pred T) f : injective f -> fclosed f A -> reflect (exists x, x \in A) (0 < fcard f A).
proof: Proof. move => injf clfA. apply: (iffP card_gt0P) => [[x /andP[]]|[x xA]]; first by exists x. exists (froot f x); rewrite inE roots_root /=; last exact: fconnect_sym. by rewrite -(closed_connect clfA (connect_root _ x)). Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)