proposition: Lemma head_long_cpring : long_cpring -> cpring = [:: node x0, x0, face (edge x0) & drop 3 cpring].
proof: Proof. move: cycle_rev_cpring; rewrite size_long_cpring head_cpring. case: cpring => [|x' [|x [|y p]]] //= cycNp _; move: cycNp. rewrite !rev_cons -!(rcons_cons, =^~ rot_cycle, rot1_cons) /= (inj_eq nodeI). by rewrite drop0 (canF_eq nodeK) => /and3P[/eqP-> /eqP-> _]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)