proposition: Lemma cpmap_bridgeless cp : cubic_prog cp -> bridgeless (cpmap cp).
proof: Proof. elim: cp => [_ | s cp IHcp]. by apply/existsP=> [] [b]; rewrite (@fconnect_cycle _ _ [::b]); case: b. case: s => // cp_ok; have bridge'G := IHcp cp_ok. - exact: bridgeless_ecpY. - by apply: bridgeless_ecpH => //; apply: cpmap_proper. exact: bridgeless_ecpU. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)