proposition: Lemma connected_by_path_join: forall g p1 p2 u v w, (connected_by_path g p1 u v) -> (connected_by_path g p2 v w) -> connected_by_path g (p1++(tail p2)) u w.
proof: Proof. intros. destruct H as [? [? ?]]. destruct H0 as [? [? ?]]. split. apply valid_upath_app_2. apply H. apply H0. rewrite H2, H3. reflexivity. split. assert (p1 = u::(tl p1)). apply hd_error_tl_repr. split. apply H1. reflexivity. rewrite H5. rewrite <- app_comm_cons. simpl. reflexivity. destruct p2 eqn:H5. inversion H4. destruct u0. simpl in *. rewrite <- app_nil_end. rewrite <- H4. rewrite H3. apply H2. simpl. apply last_err_app. simpl in H4. simpl. apply H4. 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