proposition: Lemma size_ring_cpmap cp : size (cpring (cpmap cp)) = cprsize cp.
proof: Proof. elim: cp => [|[n||||||] cp1]; rewrite ?cpring0 // /cprsize => <-. - exact: size_cpring_ecpR. - exact: size_cpring_ecpR. - by rewrite size_cpring_ecpN size_cpring_ecpU. - by rewrite 2!size_cpring_ecpN size_cpring_ecpU head_cpring. - exact: size_cpring_ecpU. - exact: size_cpring_ecpK. exact: size_cpring_ecpA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)