proposition: Lemma bridgeless_ecpH : bridgeless ecpH.
proof: Proof. have /idP X'eX := cface_ecpH (edge ecpH). have /idP := cface_ecpH (edge (face ecpH)); rewrite cface1 => fX'efX. have /idP := cface_ecpH (edge (face (face ecpH))); rewrite 2!cface1 => ffX'effX. apply/existsP => [] [] [||[||[||x]]] //; try by rewrite cfaceC. by rewrite cface_icpH bridgeless_cface. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)