proposition: Lemma rot1_cpring_ecpN : rot 1 (cpring ecpN) = (ecpN : ecpN) :: map icpN (drop 2 (rot 1 (cpring x0))).
proof: Proof. rewrite cpring_ecpN; case: ifP => [x0gt2|]. by rewrite (head_long_cpring x0gt2) /= !drop0 map_cat. by rewrite size_long_cpring; case: (cpring x0) => [|x [|y [|z p]]]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)