proposition: Lemma bridgeless_dual G : bridgeless (dual G) = loopless G.
proof: Proof. congr (~~ ~~ _ = _); apply/pred0P/pred0P => /(_ _) /= loop'G x /=. by rewrite cnodeC -(same_fconnect_finv nodeI) -{2}(finv_f edgeI x) loop'G. by rewrite (same_fconnect_finv nodeI) cnodeC -{2}(f_finv edgeI x) loop'G. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)