fact: Fixpoint cubic_prog (cp : cprog) := match cp with | [::] => true | CpR _ :: cp' => cubic_prog cp' | CpU :: cp' => cubic_prog cp' | CpY :: cp' => cubic_prog cp' | CpH :: cp' => cubic_prog cp' | _ => false end.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)