proposition: Lemma sort_drulesP r : sort_drules_spec r (sort_drules p r) (dbound1 r x).
proof: Proof. by rewrite sort_dbound1_eq; case: (sort_drules p r). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) mathcomp(bigop order ssralg ssrnum ssrint) fourcolor(hypermap geometry part)