proposition: Lemma size_ctrenum cp : size (ctrenum cp) = ctrmsize cp.
proof: Proof. elim: cp => [|[n||||||] cp IHcp] //=; rewrite -{}IHcp ?size_map //. by case: cp => //= *; rewrite size_map. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring cfmap ctree) fourcolor(cfcolor)