proposition: Lemma head_cpring : cpring = node x0 :: behead cpring.
proof: Proof. rewrite /cpring /orbit -orderSpred /= lastI rev_rcons; congr (_ :: _). by apply: nodeI; rewrite last_traject -iterS orderSpred (iter_order nodeI). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)