proposition: Lemma fits_upath_split': forall g p l e, fits_upath g l p -> In e l -> exists p1 p2 l1 l2, p = p1++p2 /\ ((last_error p1 = Some (src g e) /\ hd_error p2 = Some (dst g e)) \/ (last_error p1 = Some (dst g e) /\ hd_error p2 = Some (src g e))) /\ fits_upath g l1 p1 /\ fits_upath g l2 p2 /\ l = l1++(e::nil)++l2.
proof: Proof. induction p; intros. destruct l. contradiction. simpl in H; contradiction. destruct p; destruct l. contradiction. simpl in H; contradiction. contradiction. destruct H. destruct H0. subst e0. exists (a::nil). exists (v::p). exists nil. exists l. split. simpl. auto. split. destruct H. destruct H0; destruct H0; subst a; subst v. left; simpl; auto. right; simpl; auto. split. simpl; apply (adj_edge_vvalid g e a v H). split; auto. pose proof (IHp l e H1 H0); clear IHp. destruct H2 as [p1 [p2 [l1 [l2 ?]]]]. destruct H2 as [? [? [? [? ?]]]]. exists (a::p1). exists p2. exists (e0::l1). exists l2. split. simpl. rewrite <- H2. auto. split. destruct H3; destruct H3. left; split; auto. rewrite last_error_cons. apply H3. unfold not;intros. subst p1. inversion H3. right; split; auto. rewrite last_error_cons. apply H3. unfold not; intros. subst p1. inversion H3. split. destruct p1. destruct H3; destruct H3; inversion H3. assert (v = v0). inversion H2; auto. subst v0. split; auto. split. auto. simpl. simpl in H6. rewrite H6; 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