proposition: Lemma fits_upath_split: forall g p1 p2 l, fits_upath g l (p1++p2) -> exists l1 l2 l3, fits_upath g l1 p1 /\ fits_upath g l3 p2 /\ l = (l1++l2++l3).
proof: Proof. induction p1; intros. rewrite app_nil_l in H. exists nil. exists nil. exists l. split. simpl; auto. split; simpl; auto. destruct p1. destruct l. destruct p2. exists nil; exists nil; exists nil. split. simpl; auto. split; simpl; auto. simpl in H. contradiction. replace ((a :: nil) ++ p2) with (a::p2) in H. 2: simpl; auto. destruct p2. simpl in H; contradiction. destruct H. exists nil. exists (e::nil). exists l. split; simpl; auto. apply (adj_edge_vvalid g e a v H). destruct l. simpl in H; contradiction. destruct H. apply IHp1 in H0. destruct H0 as [l1 [l2 [l3 [? [? ?]]]]]. exists (e::l1). exists l2. exists l3. split. split; auto. split. auto. simpl. rewrite H2. 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