fact: Fixpoint simple_rec (p : seq G) : bool := if p is x :: p' then (x \notin fband p') && simple_rec p' else true.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)