fact: Fixpoint size_part (p : part) : nat := match p with | Pnil => 0 | Pcons _ _ p' => (size_part p').+1 | Pcons6 _ _ p' => (size_part p').+1 | Pcons7 _ _ _ p' => (size_part p').+1 | Pcons8 _ _ _ _ p' => (size_part p').+1 end.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap color geometry)