proposition: Lemma size_proper_cpring : proper_cpring = (1 < size cpring).
proof: Proof. move: (iter_order nodeI x0) (orbit_uniq node x0). rewrite size_cpring /proper_cpring /orbit -(orderSpred node x0). by case: _.-1 => /= [-> | n _ /andP[/norP[]] //]; rewrite eqxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)