fact: Definition mem_range r := match r return pred nat with | Pr55 => pred1 5 | Pr66 => pred1 6 | Pr77 => pred1 7 | Pr88 => pred1 8 | Pr56 => pred2 5 6 | Pr67 => pred2 6 7 | Pr78 => pred2 7 8 | Pr57 => pred3 5 6 7 | Pr68 => pred3 6 7 8 | Pr58 => pred4 5 6 7 8 | Pr59 => leq 5 | Pr69 => leq 6 | Pr79 => leq 7 | Pr89 => leq 8 | Pr99 => leq 9 end.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap color geometry)