proposition: Lemma gmedgeK : cancel3 gmedge gmnode gmface.
proof: Proof. case=> d Gd; apply/val_inj; rewrite !val_insubd /= ifE. have [_ | G'n3ed] := ifP; first by rewrite gnode4 gedge2 Gd. have [_ | G'n2ed] := ifP; first by rewrite gnode4 gedge2 Gd gmgrid_edge G'n3ed. rewrite ifT; first by rewrite gnode4 gedge2 Gd !gmgrid_edge G'n3ed G'n2ed. rewrite -gnode_face gnode4 gmgridE halfg_face in G'n3ed. do [rewrite gmgridE -implyNb => /implyP] in Gd. by rewrite gmgridE orbC -halfg_face gnodeK Gd //; case/norP: G'n3ed. 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)