proposition: Lemma cubic_ecpU : quasicubic (rev (cpring ecpU)).
proof: Proof. rewrite cpring_ecpU; apply/cubicP => u; rewrite inE /= mem_rev !inE. case: u => [||x] //=; rewrite (mem_map icpU_inj) -mem_rev => x0N'x. have [n3x x'nx] := cubicP cubicG x x0N'x; rewrite mem_rev mem_cpring in x0N'x. case: eqP => [Dx | _]; first by rewrite Dx fconnect1 in x0N'x. split; rewrite //= (inj_eq nodeI). case: eqP => /= [Dx | x0'x]; first by rewrite Dx connect0 in x0N'x. rewrite /= (inj_eq nodeI) n3x; case: eqP => // Dx. by rewrite -Dx cnodeC fconnect1 in x0N'x. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)