proposition: Lemma precubic_leq : precubic -> forall x, order node x <= 3.
proof: Proof. by move/subsetP/in1T. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)