proposition: Lemma mem_insertE : plain G -> forall p x, (x \in insertE p) = has (cedge x) p.
proof: Proof. move=> plainG p x; elim: p => //= y p <-. by rewrite cedgeC [cedge y x](plain_orbit plainG) !inE orbA. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)