proposition: Lemma dscore_cap2 (x : G) : arity x = nhub -> 0 < dscore x -> 0 < dboundK + \sum_(y in cface x) dbound2 rt rs y.
proof: Proof. move=> nFx /lt_le_trans-> //; rewrite /dscore -dboundK_eq // ler_add2l. do 2!rewrite (reindex_inj faceI) -(eq_bigl _ _ (fun y => cface1r y x)) /=. by apply: ler_sum => y xFy; rewrite dbound2_leq // -(arity_cface xFy). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) mathcomp(bigop order ssralg ssrnum ssrint) fourcolor(hypermap geometry part)