proposition: Lemma fcard1P (T : finType) (A : pred T) f : injective f -> fclosed f A -> reflect (exists2 x, x \in A & exists2 y, y \in A & ~~ fconnect f x y) (1 < fcard f A).
proof: Proof. move=> inj_f clAf; pose cfC := fconnect_sym inj_f. apply: (iffP card_gt1P) => [|[x xA [y yA not_xfy]]]. move => [x] [y] [/andP [/= rfx xA]] /andP[/= rfy yA] xDy. by exists x; try exists y; rewrite // -root_connect // (eqP rfx) (eqP rfy). exists (froot f x), (froot f y); rewrite !inE !roots_root ?root_connect //=. by split => //; rewrite -(closed_connect clAf (connect_root _ _)). Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)