proposition: Lemma ecpR1_eq (G : hypermap) x0 : ecpR 1 x0 = face (edge x0) :> G.
proof: Proof. by rewrite /= subn1 -{3}(f_finv nodeI x0) nodeK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)