fact: Fixpoint meet_part (p q : part) {struct q} : part := match q, p with | Pcons sq hq q', Pcons sp hp p' => Pcons (meet_range sp sq) (meet_range hp hq) (meet_part p' q') | Pcons sq hq q', Pcons6 hp f1 p' => Pcons6 (meet_range hp hq) f1 (meet_part p' q') | Pcons sq hq q', Pcons7 hp f1 f2 p' => Pcons7 (meet_range hp hq) f1 f2 (meet_part p' q') | Pcons sq hq q', Pcons8 hp f1 f2 f3 p' => Pcons8 (meet_range hp hq) f1 f2 f3 (meet_part p' q') | Pcons6 hq f1 q', Pcons sp hp p' => Pcons6 (meet_range hp hq) f1 (meet_part p' q') | Pcons7 hq f1 f2 q', Pcons sp hp p' => Pcons7 (meet_range hp hq) f1 f2 (meet_part p' q') | Pcons8 hq f1 f2 f3 q', Pcons sp hp p' => Pcons8 (meet_range hp hq) f1 f2 f3 (meet_part p' q') | Pcons6 hq f1q q', Pcons6 hp f1p p' => Pcons6 (meet_range hp hq) (meet_range f1p f1q) (meet_part p' q') | Pcons7 hq f1q f2q q', Pcons7 hp f1p f2p p' => Pcons7 (meet_range hp hq) (meet_range f1p f1q) (meet_range f2p f2q) (meet_part p' q') | Pcons8 hq f1q f2q f3q q', Pcons8 hp f1p f2p f3p p' => Pcons8 (meet_range hp hq) (meet_range f1p f1q) (meet_range f2p f2q) (meet_range f3p f3q) (meet_part p' q') | _, _ => p end.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap color geometry)