proposition: Lemma cubic_cube : cubic cube.
proof: Proof. unlock cube; apply/cubicP=> u _. by case: u; case; split; rewrite //= ?edgeK ?faceK ?nodeK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring)