proposition: Lemma sub_adj_icpA : subrel (adj : rel G) (adj : rel ecpA).
proof: Proof. move=> x y; case/adjP=> z xFz zRy; apply/adjP. exists z; apply: sub_cface_icpA; rewrite {x xFz}//= /ecpA_edge if_neg. case: ifP => // ex0Fnx0; do 2?case: eqP => [Dz | _] //. by rewrite cface1 nodeK -(same_cface ex0Fnx0) -Dz. by rewrite (same_cface ex0Fnx0) -(canLR nodeK Dz) -cface1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)