proposition: Lemma finite_graph_domain f: fgraph f -> (finite_set f <-> finite_set (domain f)).
proof: Proof. by move=> /Eq_domain /card_eqP; rewrite /finite_set /finite_c => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)