proposition: Lemma bridgeless_cube : bridgeless cube = bridgeless G.
proof: Proof. have [_ qfEf] := qfAf; unlock cube; congr (is_true (~~ _)). apply/existsP/existsP=> [[u uFeu] | [x xFex]]; last first. by exists (tsI CTen x); rewrite 2!cface1 -qfEf. case Du: u uFeu (closed_connect qFaQf uFeu) => [[] //= x] uFeu _. by exists x; rewrite 2!(@cface1 qmap) -qfEf in uFeu. exists (node (face x)); rewrite faceK. by rewrite (@cfaceC qmap) 2!cface1 -qfEf in uFeu. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring)