proposition: Lemma bridge_splittable: forall p g u v e, connected_by_path g p u v -> bridge g e u v -> (exists p1 p2, p = p1++p2 /\ ((connected_by_path g p1 u (src g e) /\ connected_by_path g p2 (dst g e) v) \/ (connected_by_path g p1 u (dst g e) /\ connected_by_path g p2 (src g e) v)) ).
proof: Proof. induction p; intros. destruct H. destruct H1. inversion H1. destruct p. unfold bridge in H0. assert (fits_upath g nil (a::nil)). simpl. apply (valid_upath_vvalid g (a::nil)). apply H. left; auto. apply H0 in H1; auto. contradiction. destruct H. destruct H1. simpl in H1; inversion H1. subst a. clear H1. destruct H. destruct H as [e' ?]. destruct (EE e e'). unfold equiv in e0. subst e'. destruct H. destruct H3; destruct H3; rewrite H3; rewrite H4. exists (u::nil); exists (v0::p). split. simpl; auto. left. split. split. simpl. rewrite <- H3. apply H. simpl; auto. split. apply H1. split. simpl. auto. rewrite last_error_cons in H2; auto. unfold not; intros. inversion H5. exists (u::nil); exists (v0::p). split. simpl; auto. right. split. split. simpl. rewrite <- H4. apply H. simpl; auto. split. apply H1. split. simpl. auto. rewrite last_error_cons in H2; auto. unfold not; intros. inversion H5. specialize IHp with g v0 v e. assert (exists p1 p2 : list V, v0 :: p = p1 ++ p2 /\ (connected_by_path g p1 v0 (src g e) /\ connected_by_path g p2 (dst g e) v \/ connected_by_path g p1 v0 (dst g e) /\ connected_by_path g p2 (src g e) v)). apply IHp. split. auto. split. simpl. auto. rewrite last_error_cons in H2; auto. unfold not; intros. inversion H3. unfold bridge; intros. unfold bridge in H0. assert (In e (e'::l)). apply (H0 (u::p0) (e'::l)). split. apply valid_upath_cons. apply H3. destruct H3. destruct H5. rewrite H5. simpl. exists e'; auto. split. simpl; auto. destruct H3. destruct H5. rewrite last_error_cons. auto. unfold not; intros. rewrite H7 in H5. inversion H5. destruct p0. destruct H3. destruct H5. inversion H5. destruct H3. destruct H5. simpl in H5. inversion H5. subst v1. split; auto. destruct H5. unfold complement, equiv in c. symmetry in H5; contradiction. auto. destruct H3 as [p1 [p2 [? ?]]]. exists (u::p1); exists p2. split. simpl. rewrite H3. auto. destruct H4; destruct H4. left; split; auto. split. apply valid_upath_cons. rewrite H3 in H1. apply (valid_upath_app_split _ _ _ H1). destruct H4. destruct H6. rewrite H6. simpl. exists e'. auto. split. simpl; auto. destruct H4. destruct H6. rewrite last_error_cons. auto. unfold not; intros. rewrite H8 in H6; inversion H6. right; split; auto. split. apply valid_upath_cons. rewrite H3 in H1. apply (valid_upath_app_split _ _ _ H1). destruct H4. destruct H6. rewrite H6. simpl. exists e'. auto. split. simpl; auto. destruct H4. destruct H6. rewrite last_error_cons. auto. unfold not; intros. rewrite H8 in H6; inversion H6. 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