proposition: Lemma cpmap_plain cp : cubic_prog cp -> plain (cpmap cp).
proof: Proof. elim: cp => [_ | s cp IHcp]; first by apply/plainP=> [] []. case: s => // /IHcp plainG. - exact: plain_ecpY. - exact: plain_ecpH. exact: plain_ecpU. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)