proposition: Lemma cubicP A : reflect {in A, forall x, node (node (node x)) = x /\ node x != x} (cubicb A).
proof: Proof. apply: (iffP subsetP) => cubicA x Ax. have oNx: order node x = 3 by apply/eqP; apply: cubicA. split; first by rewrite -{2}(iter_order nodeI x) oNx. by move: (orbit_uniq node x); rewrite /orbit oNx eq_sym => /andP[/norP[]]. have [n3x_x x'nx] := cubicA x Ax. have cycN3x: fcycle node (traject node x 3) by rewrite /= n3x_x !eqxx. apply/eqP/(order_cycle cycN3x); last exact: mem_head. by rewrite /= !inE negb_or -{3}n3x_x !(inj_eq nodeI) eq_sym x'nx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)