proposition: Lemma cubic_mirror : cubic (mirror G) = cubic G.
proof: Proof. congr (is_true _); apply: eq_subset_r => x. by rewrite !inE /= (order_finv nodeI). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)