proposition: Lemma forest_adj_bridge: forall g e u v, uforest' g -> adj_edge g e u v -> bridge g e u v.
proof: Proof. unfold bridge; intros. apply (upath_simplifiable_edges g p l u v) in H2; auto. destruct H2 as [p' [l' [? [? [? [? ?]]]]]]. assert (fits_upath g (e::nil) (u::v::nil)). simpl. split; auto. apply connected_by_path_vvalid in H1; apply H1. assert (connected_by_path g (u::v::nil) u v). apply connected_exists_list_edges'. apply connected_by_path_vvalid in H1. intros. simpl in H8. destruct H8. subst v0. apply H1. destruct H8. subst v0. apply H1. contradiction. exists (e::nil). auto. simpl; auto. simpl; auto. assert (simple_upath g (u::v::nil)). split. apply H8. apply NoDup_cons. unfold not; intros. destruct H9. subst u. apply forest_no_self_adjacency in H0; auto. contradiction. apply NoDup_cons. auto. apply NoDup_nil. assert (p' = (u::v::nil)). destruct H as [? [? [? ?]]]. apply (H12 u v); auto. subst p'. apply H6. assert (l' = (e::nil)). apply (uforest'_unique_lpath (u::v::nil) _ _ g); auto. rewrite H10. left; 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