proposition: Lemma frestrict_inj : {in P&, injective f} -> injective frestrict.
proof: Proof. move => inj_f x y. move/(f_equal val); rewrite !val_frestrict. move/inj_f/val_inj => -> //; exact: valP. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)