proposition: Lemma D4_plain : plain D4.
proof: Proof. apply/plainP => x _; rewrite (rwP eqP) (rwP andP); move: x. by apply/forallP; rewrite forall_all_ord. Qed.
imports: mathcomp(all_ssreflect) fourcolor(hypermap geometry) GraphTheory(preliminaries digraph sgraph) GraphTheory(hmap_ops embedding)