proposition: Lemma cpring_ecpH : cpring ecpH = [:: node ecpH, ecpH : ecpH & map icpH (drop 2 (cpring x0))].
proof: Proof. rewrite -drop2_cpring_ecpH -head_proper_cpring //. by rewrite size_proper_cpring size_cpring_ecpH -size_proper_cpring. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)