proposition: Lemma drop2_cpring_ecpY : drop 2 (cpring ecpY) = map icpY (behead (cpring x0)).
proof: Proof. by rewrite cpring_ecpN cpring_ecpU head_cpring /= !drop0 -map_comp. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)