proposition: Lemma fcard_gt0P (a : {pred T}) : fclosed f a -> reflect (exists x, x \in a) (0 < fcard f a).
proof: Proof. move=> 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: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)