proposition: Lemma bridge_must_be_crossed: forall g e u v p l, bridge g e u v -> In u p -> In v p -> fits_upath g l p -> In e l.
proof: Proof. intros. assert (exists p' l', connected_by_path g p' u v /\ fits_upath g l' p' /\ incl p' p /\ incl l' l). apply fits_upath_reduced_list; auto. destruct H3 as [p' [l' [? [? [? ?]]]]]. apply H6. apply (H p' l'); auto. Qed.
imports: Coq.Logic.Classical CertiGraph.lib.List_ext CertiGraph.lib.EquivDec_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_relation CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.FiniteGraph