proposition: Lemma D4_embedding : embedding D4_g.
proof: Proof. split; first exact D4_plain. - move=> x. apply/codomP. setoid_rewrite (rwP eqP). apply/existsP; rewrite exists_has_ord. move: x. apply/forallP. rewrite forall_all_ord. reflexivity. - move => x y. rewrite connectEord (rwP eqP). move: y; apply/forallP; rewrite forall_all_ord. move: x; apply/forallP; rewrite forall_all_ord. reflexivity. - move => x y. rewrite /adjn; under eq_existsb => z do rewrite !inE !connectEord. rewrite exists_has_ord (rwP eqP). move: y; apply/forallP; rewrite forall_all_ord. move: x; apply/forallP; rewrite forall_all_ord. reflexivity. Qed.
imports: mathcomp(all_ssreflect) fourcolor(hypermap geometry) GraphTheory(preliminaries digraph sgraph) GraphTheory(hmap_ops embedding)