proposition: Lemma plain_dual : plain (dual G) = plain G.
proof: Proof. congr (is_true _); apply: eq_subset_r => x. by rewrite /order_set /in_mem /= (order_finv edgeI). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)