proposition: Lemma srcycleI : bridgeless G -> forall r, scycle rlink r = srcycle r.
proof: Proof. move=> bridge'G [|x0 p] //; rewrite /scycle simple_recI /=; congr (is_true _). elim: p {1 3 5}x0 => [|y p IHp] x /=; first by rewrite !andbT. rewrite -{}IHp -!andbA unfold_in /=; apply: andb_id2l => exFy. bool_congr; congr (_ && _); rewrite cfaceC -(same_cface exFy) cfaceC. by rewrite bridgeless_cface // -all_predC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)