proposition: Lemma cface_ecpH u : cface ecpH u = (u \in [:: ecpH : ecpH; face ecpH; face (face ecpH)]).
proof: Proof. by apply: fconnect_cycle; rewrite //= nodeK (negPf x0gt1). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)