proposition: Lemma bridgeless_patch : bridgeless Gd -> bridgeless Gr -> chordless bGd -> bridgeless G.
proof: Proof. move=> bridge'Gd bridge'Gr chord'Gd; apply/existsP=> [[x xFex]]. have [/imageP[xr _ Dx] | ] := boolP (x \in codom hr). by case/existsP: bridge'Gr; exists xr; rewrite patch_face_r hrE -Dx. rewrite im_hr => /norP[/negbNE/imageP[xd _ Dx]]. rewrite Dx /= (mem_map Ihd) => b'xd; rewrite Dx -hdE // in xFex. have [out_x | out'x] := boolP (hd xd \in outer); last first. by case/existsP: bridge'Gd; exists xd; rewrite patch_face_d. have: hd (edge xd) \in outer by rewrite -(closed_connect closed_outer xFex). move: out_x; rewrite !outer_hd => /hasP[yd b_yd xFyd] /hasP[zd b_zd exFzd]. case/exists_inP: (subsetP chord'Gd _ b_yd); exists zd; rewrite !inE /=. by apply/adjP; exists xd; first by rewrite cfaceC. have [[yr Dyr Dnyr] [cEbd _]] := (bGdP b_yd, andP cycEbGd). apply/and3P; split=> //; apply/eqP=> Dzd; case/existsP: bridge'Gr. exists (node yr); rewrite cface1r nodeK. rewrite patch_face_r -Dnyr -Dyr (eqP (next_cycle cEbd b_yd)) -Dzd. by rewrite -(same_cface (patch_face_d' xFyd)) (same_cface xFex) patch_face_d'. exists (node (node yr)); rewrite cface1r nodeK patch_face_r -Dnyr cfaceC. rewrite -(same_cface (patch_face_d' xFyd)) (same_cface xFex). suffices /eqP <-: hd zd == hr (node (node yr)) by apply: patch_face_d'. by rewrite -hdErN -Dnyr Dzd (eqP (prev_cycle cEbd b_yd)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry jordan color coloring)