proposition: Lemma cpmap_cubic cp : cubic_prog cp -> quasicubic (rev (cpring (cpmap cp))).
proof: Proof. elim: cp => [_ | s cp IHcp]; first by rewrite cpring0; apply/cubicP=> [] []. case: s => // [n|||] /IHcp cubicG. - exact: cubic_ecpR. - exact: cubic_ecpY. - exact: cubic_ecpH. exact: cubic_ecpU. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)