proposition: Lemma dboundK_eq : dboundK = 60%:Z - (10 * arity x)%:Z.
proof: Proof. rewrite -(subnKC (pentaG x)) nFx /dboundK; case: (nhub - 5)%N => // m. by rewrite -addSnnS mulnDr PoszD opprD addNKr mulnC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) mathcomp(bigop order ssralg ssrnum ssrint) fourcolor(hypermap geometry part)