proposition: Lemma eqm_bridgeless : bridgeless G = bridgeless G'.
proof: Proof. congr (~~ _ = _); case: G eqG => [d e n f GeK] [e' n' f' G'eK /= eqE _ eqF]. by apply: eq_existsb => x; rewrite eqE; apply: eq_fconnect. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)