proposition: Lemma valid_path_split: forall g p1 p2, paths_meet g p1 p2 -> valid_path g (p1 +++ p2) -> valid_path g p1 /\ valid_path g p2.
proof: Proof. intros g p1. destruct p1 as [v1 p1]. revert v1. induction p1; intros; destruct p2 as [v2 p2]; unfold path_glue, fst, snd in H0. + split. - simpl in H0 |-* . destruct p2; auto. destruct H0. subst. simpl in H1. destruct p2; [|destruct H1 as [H1 _]]; destruct H1 as [_ [H1 _]]; apply H1. - rewrite app_nil_l in H0. destruct H as [x [? ?]]. simpl in H, H1. subst v1. subst v2. auto. + specialize (IHp1 (dst g a) (v2, p2)). unfold path_glue, fst, snd in IHp1. rewrite <- app_comm_cons in H0. specialize (IHp1 (paths_meet_cons _ _ _ _ _ H) (valid_path_cons _ _ _ _ H0)). destruct IHp1. split; auto. clear H2 H. destruct H0. split; auto. simpl in *. destruct p1. destruct (nil ++ p2); intuition. split; auto. destruct ((e :: p1) ++ p2); intuition. Qed.
imports: Coq.Logic.ProofIrrelevance Coq.micromega.Lia CertiGraph.lib.Coqlib CertiGraph.lib.EnumEnsembles CertiGraph.lib.List_ext CertiGraph.lib.EquivDec_ext CertiGraph.graph.graph_model Coq.Lists.List Coq.Lists.ListDec