proposition: Lemma cubic_orbit : cubic -> forall x y, cnode x y = (y \in [:: x; node x; node (node x)]).
proof: Proof. by move/subsetP=> cubicG x y; rewrite fconnect_orbit /orbit (eqnP (cubicG x _)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)