proposition: Lemma cfmap_long cp : config_prog cp -> long_cpring (cpmap cp).
proof: Proof. rewrite size_long_cpring; elim: cp => [|s cp IHcp] //=. case: s => // [n||]; rewrite ?size_cpring_ecpR ?size_cpring_ecpH //. rewrite size_cpring_ecpY. by case: cp => [|s cp] in IHcp * => [_ | /IHcp/leqW//]; rewrite cpring0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)