fact: Fixpoint insertE (p : seq G) : seq G := if p is x :: p' then [:: x, edge x & insertE p'] else [::].
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)