proposition: Lemma adj_icpN : let adjx0 x y := cface (edge (face (edge x0))) x && cface x0 y in forall x y, adj (icpN x) (icpN y) = [|| adj x y, adjx0 x y | adjx0 y x].
proof: Proof. move=> /= x y; apply/adjP/idP=> [[[||z] xFz zRy]|]. - rewrite cface1r /= cface_icpN cfaceC in xFz. by rewrite xFz orbA orbC -cface_icpN cface1 /= eqxx [fconnect _ _ _]zRy. - rewrite [rlink _ _]cface1 cface_icpN in zRy. by rewrite zRy -cface_icpN cface1 cfaceC /= eqxx xFz orbT. - by case: adjP => // [[]]; exists z; rewrite /rlink -cface_icpN. case/or3P=> [/adjP[z xFz zRy] | /andP[zFx zFy] | /andP[zFy zFx]]. - by exists (icpN z); rewrite /rlink cface_icpN. - exists (edge ecpN); last by rewrite /rlink cface1 cface_icpN. by rewrite cfaceC -cface_icpN cface1r /= eqxx in zFx. exists (ecpN : ecpN); first by rewrite cfaceC cface1 cface_icpN. by rewrite -cface_icpN cface1 /= eqxx in zFy. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)