proposition: Lemma sort_dbound1_eq ru: let rup := sort_drules p ru in dbound1 ru x = (rup + dbound1 rup x)%N.
proof: Proof. rewrite /= -[dbound1 _ _]addn0 -[0%N]/(0 + count (fitp x) [::])%N /sort_drules. elim: ru 0%N [::] => //= r ru IHru m ru'. rewrite (fitp_cmp fit_xp); case eq_pr: (cmp_part p r); rewrite //= -{}IHru. by rewrite -addnA 2!(addnCA (fitp x r)). by rewrite addnS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) mathcomp(bigop order ssralg ssrnum ssrint) fourcolor(hypermap geometry part)