proposition: Lemma size_cpring_ecpK : size (cpring ecpK) = (size (cpring x0)).-2.+1.
proof: Proof. by rewrite /ecpK size_cpring_ecpR size_cpring_ecpN /ecpR' size_cpring_ecpR /=. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)