fact: Fixpoint cat_part (p q : part) : part := match p with | Pcons s h p' => Pcons s h (cat_part p' q) | Pcons6 h f1 p' => Pcons6 h f1 (cat_part p' q) | Pcons7 h f1 f2 p' => Pcons7 h f1 f2 (cat_part p' q) | Pcons8 h f1 f2 f3 p' => Pcons8 h f1 f2 f3 (cat_part p' q) | Pnil => q end.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap color geometry)