proposition: Lemma patch_fcard_face_d : fcard face Gd = size bG + fcard face (predC Fbd).
proof: Proof. by rewrite size_map -(scycle_fcard_fband cycEbGd) -n_compC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry jordan color coloring)