proposition: Lemma size_cpring_ecpH : size (cpring ecpH) = size (cpring x0).
proof: Proof. by rewrite /ecpH size_cpring_ecpN size_cpring_ecpY head_cpring. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)