proposition: Lemma dbound1_eq : dscore1 (face (face x)) = dbound1 rs x.
proof: Proof. congr _%:Z; rewrite /rs /source_drules; case: rf => _ _ []. elim: the_drules => //= r dr ->. by rewrite /exact_fitp /inv_face2 !faceK nFx eq_sym; case: ifP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) mathcomp(bigop order ssralg ssrnum ssrint) fourcolor(hypermap geometry part)