proposition: Lemma forest_simple_bridge: forall p l g u v, uforest' g -> connected_by_path g p u v -> simple_upath g p -> fits_upath g l p -> forall e, In e l -> bridge g e u v.
proof: Proof. induction p; intros. destruct H0. destruct H4. inversion H4. destruct p; destruct l. contradiction. simpl in H2. contradiction. simpl in H2. contradiction. assert (a = u). destruct H0. destruct H4. inversion H4. auto. subst a. unfold bridge; intros. pose proof (upath_simplifiable_edges g p0 l0 u v H4 H5). destruct H6 as [p' [l' [? [? [? [? ?]]]]]]. apply H10. assert (p' = (u::v0::p)). assert (unique_simple_upath g). apply H. apply (H11 u v p' (u::v0::p)); auto. subst p'. assert ((e0::l) = l'). apply (uforest'_unique_lpath (u::v0::p) (e0::l) l' g); auto. subst l'. apply H3. 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