proposition: Lemma simple_map (G G' : hypermap) (h : G -> G') : (forall x y, cface (h x) (h y) = cface x y) -> forall p, simple (map h p) = simple p.
proof: Proof. move=> eq_hF; elim=> [|x p IHp] //; rewrite map_cons !simple_cons {}IHp. by congr (~~ _ && _); elim: p => // y p IHp; rewrite !fband_cons eq_hF IHp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)