proposition: Lemma fits_upath_app: forall g p1 p2 l1 l2 e u v, fits_upath g l1 p1 -> fits_upath g l2 p2 -> last_error p1 = Some u -> hd_error p2 = Some v -> adj_edge g e u v -> fits_upath g (l1++(e::nil)++l2) (p1++p2).
proof: Proof. induction p1; intros. inversion H1. destruct p1. destruct l1. simpl. destruct p2. inversion H2. simpl in H1. inversion H1. subst a. simpl in H2. inversion H2. subst v0. split; auto. simpl in H; contradiction. destruct l1. simpl in H; contradiction. split. apply H. apply (IHp1 p2 l1 l2 e u v); auto. apply H. 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