proposition: Lemma plain_ecpU : plain ecpU.
proof: Proof. apply/plainP=> [] [||x] // _; have [eex x'ex] := plainP plainG x isT. by rewrite -!icpN_edge eex. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)