proposition: Lemma planar_bridgeless_grid_map : planar_bridgeless grid_map.
proof: Proof. rewrite /grid_map; case: has_cutout => G h r planG Ih hE _ hN Dr cycNr. split; rewrite ?planar_dual ?bridgeless_dual //; apply/existsP=> -[x xNex]. without loss bb_hx: x xNex / h x \in gm_inner. move=> IHx; have:= valP (h x); rewrite gmgridE => /orP[/IHx[]//|bb_ex]. apply: IHx (edge x) _ _; [rewrite cnodeC | by rewrite hE]. by congr (cnode _ _): xNex; apply/Ih/val_inj; rewrite !hE /= gedge2. have [/existsP[i ri_x] | r'x] := boolP [exists i, x \in r i]. have /andP[cycNri _] := cycNr i isT. have:= xNex; rewrite (fconnect_cycle cycNri) //; move: ri_x. rewrite -!(mem_map Ih) hE -!(mem_rev (map h _)) Dr -!(mem_map val_inj). by rewrite val_gmring // !in_mring !inE => /andP[_ /negPf->]. suff: halfg (h x) = halfg (h (edge x)) by apply/eqP; rewrite hE neq_halfg_edge. case/connectP: xNex => _ /fpathP[k ->] ->; rewrite last_traject. rewrite negb_exists in r'x; elim: k => // k IHk in x bb_hx r'x *. rewrite -(gnodeK (h x)) halfg_face iterSr. rewrite -IHk ?hN ?val_gmnode ?gm_inner_node //. apply/forallP=> i; apply: contra (forallP r'x i). by move/(fconnect_cycle (ucycle_cycle (cycNr i isT))) <-; rewrite -cnode1. 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)