proposition: Lemma dscore_cap1 (m : nat) : (forall y : G, dscore1 y <= m) -> forall x : G, 0 < dscore x -> forall d, (59 < (10 - m) * d -> arity x < d)%N.
proof: Proof. move=> ub_m x pos_x d max_m; apply: contraLR pos_x; rewrite -leqNgt => ledx. have ltm10: (m < 10)%N by rewrite -subn_gt0; case: (10 - m)%N max_m. have{max_m}: 60%:Z <= ((10 - m) * arity x)%:Z. by rewrite lez_nat (leq_trans max_m) ?leq_mul. rewrite -leNgt -ler_subr_addr ler_subl_addl add0r => /le_trans-> //. rewrite !PoszM -!mulrzz -![_ *~ _]sumr_const -sumrB ler_sum // => y _. rewrite -(ler_add2r m%:Z) -PoszD subnK 1?ltnW // addrAC. by rewrite ler_subr_addr ler_add2l ler_subl_addr ler_paddr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) mathcomp(bigop order ssralg ssrnum ssrint) fourcolor(hypermap geometry part)