proposition: Lemma fits_upath_split2: forall g p l e u v, connected_by_path g p u v -> fits_upath g l p -> In e l -> exists p1 p2 l1 l2, 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)) /\ fits_upath g l1 p1 /\ fits_upath g l2 p2 /\ l = l1++(e::nil)++l2.
proof: Proof. intros. destruct (fits_upath_split' g p l e) as [p1 ?]; auto. destruct H2 as [p2 [l1 [l2 [? [? [? [? ?]]]]]]]. exists p1. exists p2. exists l1. exists l2. repeat split; auto. destruct H. destruct H7. subst p; subst l. destruct H3. ++ destruct H2. left. split. split. apply (fits_upath_valid_upath g p1 l1); auto. split. destruct p1. inversion H2. simpl; auto. auto. split. apply (fits_upath_valid_upath g p2 l2); auto. split. auto. destruct p2. inversion H3. rewrite last_err_split2 in H8. auto. ++ destruct H2. right. split. split. apply (fits_upath_valid_upath g p1 l1); auto. split. destruct p1. inversion H2. simpl; auto. auto. split. apply (fits_upath_valid_upath g p2 l2); auto. split. auto. destruct p2. inversion H3. rewrite last_err_split2 in H8. 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