proposition: Lemma hiso_fcard (f : G -> G) (f' : H -> H) : injective f -> (forall x, i (f x) = f' (i x)) -> fcard f G = fcard f' H.
proof: Proof. move => inj_f com_f_f'. have inj_f' : injective f'. { move => x y. rewrite -{1}[x](bijK' i) -{1}[y](bijK' i) -!com_f_f'. by move/(bij_injective i)/inj_f/(bij_injective' i). } suff adj : fun_adjunction i f' f H. { rewrite (adjunction_n_comp _ _ _ _ adj) //; exact: fconnect_sym. } apply: comm_adj => //= x y. by rewrite -com_f_f' inj_eq. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)