proposition: Lemma hiso_plain : plain G = plain H.
proof: Proof. congr (is_true _); apply/plainP/plainP. - move => plainG x _; have [G1 G2] := plainG (i^-1 x) isT. by rewrite -[x](bijK' i) -!hiso_edge G1 inj_eq. - move => plainH x _; have [H1 H2] := plainH (i x) isT. rewrite -!hiso_edge inj_eq // in H1 H2. by rewrite H2 (bij_injective i H1). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)