fact: Fixpoint cmp_part (p q : part) {struct q} : part_rel := match q, p with | Pcons sq hq q', Pcons sp hp p' => meet_prel (cmp_range sp sq) (meet_prel (cmp_range hp hq) (cmp_part p' q')) | Pcons sq hq q', Pcons6 hp _ p' => meet_prel (cmp_range Pr66 sq) (meet_prel (cmp_range hp hq) (cmp_part p' q')) | Pcons sq hq q', Pcons7 hp _ _ p' => meet_prel (cmp_range Pr77 sq) (meet_prel (cmp_range hp hq) (cmp_part p' q')) | Pcons sq hq q', Pcons8 hp _ _ _ p' => meet_prel (cmp_range Pr88 sq) (meet_prel (cmp_range hp hq) (cmp_part p' q')) | Pcons6 hq _ q', Pcons sp hp p' => meet_prel (notPsubset (cmp_range sp Pr66)) (meet_prel (cmp_range hp hq) (cmp_part p' q')) | Pcons7 hq _ _ q', Pcons sp hp p' => meet_prel (notPsubset (cmp_range sp Pr77)) (meet_prel (cmp_range hp hq) (cmp_part p' q')) | Pcons8 hq _ _ _ q', Pcons sp hp p' => meet_prel (notPsubset (cmp_range sp Pr88)) (meet_prel (cmp_range hp hq) (cmp_part p' q')) | Pcons6 hq f1q q', Pcons6 hp f1p p' => meet_prel (cmp_range hp hq) (meet_prel (cmp_range f1p f1q) (cmp_part p' q')) | Pcons7 hq f1q f2q q', Pcons7 hp f1p f2p p' => meet_prel (cmp_range hp hq) (meet_prel (cmp_range f1p f1q) (meet_prel (cmp_range f2p f2q) (cmp_part p' q'))) | Pcons8 hq f1q f2q f3q q', Pcons8 hp f1p f2p f3p p' => meet_prel (cmp_range hp hq) (meet_prel (cmp_range f1p f1q) (meet_prel (cmp_range f2p f2q) (meet_prel (cmp_range f3p f3q) (cmp_part p' q')))) | Pnil, _ => Psubset | _, Pnil => Pstraddle | _, _ => Pdisjoint end.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap color geometry)