proposition: Lemma bridgeless_mirror G : bridgeless (mirror G) = bridgeless G.
proof: Proof. congr (~~ ~~ _ = _); apply/pred0P/pred0P => [] /(_ _) /= bridge'G x /=. rewrite cfaceC -{2}[x]edgeK cface1 cface1r -(same_fconnect_finv faceI). exact: bridge'G. rewrite (same_fconnect_finv faceI) cfaceC /comp -cface1 -{2}[x]nodeK -cface1r. exact: bridge'G. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)