proposition: Lemma adj_no_cface : bridgeless G -> forall x y, adj x y -> cface x y = false.
proof: Proof. move=> bridge'G x y /adjP[z xFz zRy]; rewrite cfaceC -(same_cface zRy) cfaceC. by rewrite (same_cface xFz) bridgeless_cface. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)