proposition: Lemma colorable_bridgeless : four_colorable -> bridgeless G.
proof: Proof. case=> k [kE kF]; apply/existsP => [[x eFex]]; case/negP: (kE x); apply/eqP. by rewrite -(fconnect_invariant kF eFex). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap walkup geometry color chromogram)