proposition: Lemma fcardEord f : injective f -> fcard f 'I_n = fcard_ord f.
proof: Proof. have eq_f : frel f =2 grel (fun x => [:: f x]). by move => u v; rewrite /= !inE eq_sym. move=> inj_f; rewrite (eq_n_comp (eq_connect eq_f)). rewrite -(eq_n_comp_r ord_enum_eqT). rewrite (n_comp_dfsP (k := n)) ?card_ord //. - apply: eq_connect_sym eq_f _. exact: fconnect_sym. - move => x y. by rewrite !ord_enum_eqT. Qed.
imports: mathcomp(all_ssreflect) fourcolor(hypermap geometry) GraphTheory(preliminaries digraph sgraph) GraphTheory(hmap_ops embedding)