proposition: Lemma gcol_cface : coloring k0 -> let k z := k0 (@injcp cp1 cp2 z) in forall x y, cface x y -> k x = k y.
proof: Proof. move=> [_ k0F] k x y xFy; apply: (fconnect_invariant k0F). exact: sub_cface_injcp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring cfmap ctree)