proposition: Lemma cubic_ecpR : quasicubic (rev (cpring ecpR)).
proof: Proof. apply: etrans cubicG; apply: eq_subset => x; congr (~~ _). by rewrite /= cpring_ecpR 2!mem_rev mem_rot. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)