proposition: Lemma good_path_unique_edge: forall (g: Gph) P p s t e, path_ends g p s t -> good_path g P p -> In e (snd p) -> exists p1 p2, Subpath g (s, p1 ++ e :: p2) p /\ path_ends g (s, p1 ++ e :: p2) s t /\ good_path g P (s, p1 ++ e :: p2) /\ ~ In e p1 /\ ~ In e p2 /\ length (p1 ++ e :: p2) <= length (snd p).
proof: Proof. intros. destruct H0. pose proof H0. eapply valid_path_unique_edge in H0; eauto. destruct H0 as [p1 [p2 [? [? [? [? [? ?]]]]]]]. exists p1, p2. do 4 (split; auto). apply path_prop_subpath with p; trivial. 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