proposition: Lemma size_long_cpring : long_cpring = (2 < size cpring).
proof: Proof. move: (orderSpred node x0) (iter_order nodeI x0) (orbit_uniq node x0). rewrite size_cpring /long_cpring (canF_eq (canF_sym nodeK)) /orbit. case: (order node x0) => [|[|[|n]]] //= _ Dnx; try by rewrite !Dnx eqxx. by case/andP => /norP[_ /norP[]]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)