proposition: Lemma dbound2_leq : dscore2 (face (face x)) <= dbound2 rt rs x.
proof: Proof. rewrite /dbound2 -dbound1_eq ler_add2r lez_nat. set y := inv_face2 _; rewrite /rt /target_drules; case: rf => _ _ []. elim: the_drules => //= r dr IHdr; case Dr': (converse_part r) => [u r']. case Hyr: (exact_fitp y r). move: (fitp_converse geoG Hyr); rewrite Dr' => /andP[]. by rewrite {1 2}/y /inv_face2 !nodeK De2 !faceK nFx => -> /= ->. by case: (u nhub) => //=; case: (fitp x r') => //; apply: ltnW. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) mathcomp(bigop order ssralg ssrnum ssrint) fourcolor(hypermap geometry part)