proposition: Lemma D4_planar : planar D4.
proof: Proof. rewrite /planar/genus/Euler_lhs/Euler_rhs. rewrite (n_compEord (@glinkC D4)) (fcardEord (@faceI D4)). by rewrite (fcardEord (@edgeI D4)) (fcardEord (@nodeI D4)) card_ord. Qed.
imports: mathcomp(all_ssreflect) fourcolor(hypermap geometry) GraphTheory(preliminaries digraph sgraph) GraphTheory(hmap_ops embedding)