proposition: Lemma plain_mirror : plain (mirror G) = plain G.
proof: Proof. congr (is_true _); apply/subsetP/subsetP=> plainG x _; rewrite !inE. by rewrite -[x]edgeK -order_mirror_edge; apply: plainG. by rewrite /order_set order_mirror_edge; apply: plainG. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)