proposition: Lemma cpring_ecpY : cpring ecpY = [:: node ecpY, ecpY : ecpY & map icpY (behead (cpring x0))].
proof: Proof. by rewrite -drop2_cpring_ecpY -head_proper_cpring. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)