proposition: Lemma patch_bridgeless : bridgeless G -> bridgeless Gd /\ bridgeless Gr.
proof: Proof. move=> br'G; do [split; apply: contra br'G => /existsP[]] => [xd | xr] xFex. apply/existsP; exists (hd xd). by rewrite -{2}[xd]edgeK hdN cface1r nodeK patch_face_d' -?cface1r. by apply/existsP; exists (hr xr); rewrite -hrE -patch_face_r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry jordan color coloring)