fact: Definition meet_prel c c' := match c with | Pdisjoint => c | Psubset => c' | Pstraddle => notPsubset c' end.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap color geometry)