proposition: Lemma comm_adj (e' : rel H) (e : rel G) (a : pred H) : (forall x y, e' (i x) (i y) = e x y) -> rel_adjunction i e' e a.
proof: Proof. move => com. constructor; first by move => x _; exists (i^-1 x); rewrite bijK'. move => x' y' _. apply/idP/idP; case/connectP. - move => p pth_p ->. elim: p x' pth_p => //= z' p IHp x' /andP [E pth_p]. rewrite -com in E. exact: connect_trans (connect1 E) (IHp _ pth_p). - move => p pth_p I. rewrite -[y'](bijK i) {}I. elim: p x' pth_p => //= [x' _|z' p IHp x' /andP [E pth_p]]; first by rewrite bijK. rewrite -[z'](bijK' i) com in E. apply: connect_trans (connect1 E) _. rewrite -[z'](bijK' i) in pth_p. move/IHp in pth_p. by rewrite bijK' in pth_p. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)