proposition: Lemma cpring_ecpK : cpring ecpK = node ecpK :: map icpK (drop 2 (cpring x0)).
proof: Proof. rewrite cpring_ecpR rot1_cpring_ecpN ecpR1_eq edgeK cpring_ecpR -subn1. by rewrite -size_cpring rotrK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)