proposition: Lemma size_cpker cp : config_prog cp -> size (cpker cp) = cpksize cp.
proof: Proof. elim: cp => // [[] //=] cp IHcp cp_ok. by rewrite size_map; case: cp IHcp cp_ok. rewrite (head_proper_cpring (cpmap_proper (config_prog_cubic _))) //=. by rewrite size_map IHcp. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)