proposition: Lemma patch_fcard_face_r : fcard face Gr = fcard face outer.
proof: Proof. rewrite /= (adjunction_n_comp hr cfaceC cfaceC closed_outer). by apply: eq_card => xr; rewrite !inE mem_closure ?codom_f. split=> [x out_x | xr yr _]; last exact: patch_face_r. apply: sigW; have [y /= xFy /imageP[yr _ Dy]] := exists_inP out_x. by exists yr; rewrite -Dy. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry jordan color coloring)