proposition: Lemma gmdart_planar : planar gmdart_map.
proof: Proof. rewrite /planar -leqn0 (@half_leq _ 1) // leq_subLR addn1. rewrite /Euler_lhs (eqnP gmdart_connected) add2n ltnS -ltn_double -addnn //. rewrite doubleD -muln2 (fcard_order_set edgeI gmdart_plain) // ltn_add2l. rewrite card_gmdart ltn_double muln2 -addnn -addnA addnAC addnA -mulnSr. by rewrite -addSn -addnS -mulSnr addnC leq_add ?fcard_gmnode// fcard_gmface. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph order ssralg ssrnum ssrint) fourcolor(hypermap geometry color coloring patch snip grid) fourcolor(matte)