proposition: Lemma fits_upath_concat: forall g p l e u, fits_upath g l p -> (exists v, last_error p = Some v /\ adj_edge g e u v) -> fits_upath g (l+::e) (p+::u).
proof: Proof. induction p; intros. destruct l. destruct H0 as [v [? ?]]. simpl in H0. inversion H0. simpl in H. contradiction. destruct p; destruct l. destruct H0 as [v [? ?]]. simpl in H0. inversion H0. subst a. simpl. split. apply adj_edge_sym; auto. apply (adj_edge_vvalid g e u v H1). simpl in H. contradiction. simpl in H. contradiction. destruct H0 as [v0 [? ?]]. destruct H. split. auto. apply IHp. auto. exists v0. split. rewrite last_error_cons in H0; auto. unfold not; intros; inversion H3. 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