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