proposition: Lemma cpmap_proper cp : cubic_prog cp -> proper_cpring (cpmap cp).
proof: Proof. rewrite size_proper_cpring. elim: cp => [|s cp IHcp] /=; first by rewrite cpring0. case: s => // [n|||] /IHcp x0gt1. - by rewrite size_cpring_ecpR. - by rewrite size_cpring_ecpY ltnW. - by rewrite size_cpring_ecpH. by rewrite size_cpring_ecpU. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)