proposition: Lemma gcol_adj : coloring k0 -> let k x := k0 (@injcp cp1 cp2 x) in forall x p, (forall y, adj x y = (y \in fband p)) -> all (fun y => k y != k x) p.
proof: Proof. move=> [k0E k0F] /= x p Dp /=; apply/allP => y py; apply/negPf. have{Dp py} xAy: adj x y by rewrite Dp (subsetP (ring_fband p)). have{xAy} /adjP[u xFu uRy] := sub_adj_injcp cp1 xAy. rewrite (fconnect_invariant k0F xFu) -(fconnect_invariant k0F uRy). exact: k0E. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring cfmap ctree)