proposition: Lemma fcard_skip : (f z == z) + fcard skip tG' = fcard f G.
proof: Proof. have symf := fconnect_sym injf; have symf' := fconnect_sym inj_skip. pose a := fconnect f z. have Cfa': fclosed f (predC a) by apply/predC_closed/connect_closed. have adj_f: fun_adjunction val f skip (predC a). apply: (strict_adjunction symf' Cfa' val_inj) => [|u v a'u]. apply/subsetP=> x a'x; apply: (codom_f _ (inG' _)). by apply: contraNneq a'x => ->; apply: connect0. by apply/base_skip/(contraNneq _ a'u) => -> /=; rewrite !inE /a fconnect_finv. rewrite (n_compC a) (n_compC (preim val a)) {3}/a (n_comp_connect symf). rewrite (adjunction_n_comp _ symf symf' Cfa' adj_f) addnA; congr (_ + _). have [fz_z | z'fz] := altP (f z =P z). have /fconnect_cycle-cyc_z: fcycle f [:: z] by rewrite /= fz_z eqxx. by apply/eqP/pred0P=> u /=; rewrite andbC [u \in preim val a]cyc_z inE ?z'G'. apply: etrans (n_comp_connect symf' (inG' z'fz)). by apply: eq_n_comp_r => u; rewrite !inE fconnect_skip -same_fconnect1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap)