fact: Fixpoint sort_drules_rec n (rs r : drules) : sort_drules_result := if r is p' :: r' then match cmp_part p p' with | Psubset => sort_drules_rec n.+1 rs r' | Pstraddle => sort_drules_rec n (p' :: rs) r' | Pdisjoint => sort_drules_rec n rs r' end else SortDrules n rs.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) mathcomp(bigop order ssralg ssrnum ssrint) fourcolor(hypermap geometry part)