proposition: Lemma simple_recI : simple =1 simple_rec.
proof: Proof. rewrite /simple; elim=> //= x p ->; congr (~~ _ && _). by apply/mapP/hasP=> [] [y py /(rootP cfaceC)]; exists y. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)