fact: Fixpoint cprsize (cp : cprog) := match cp with | [::] => 2 | CpY :: cp' => (cprsize cp').+1 | CpU :: cp' => (cprsize cp').+2 | CpK :: cp' => (cprsize cp').-2.+1 | CpA :: cp' => sub2ifgt2 (cprsize cp') | _ :: cp' => cprsize cp' end.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)