proposition: Lemma drop2_cpring_ecpH : drop 2 (cpring ecpH) = map icpH (drop 2 (cpring x0)).
proof: Proof. rewrite cpring_ecpN size_long_cpring size_cpring_ecpY. rewrite (drop_behead 3) iterS -drop_behead drop2_cpring_ecpY. by case: (cpring x0) => [|y1 [|y2 [|y3 r]]] //=; rewrite -map_comp. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)