proposition: Lemma lst_valid_path_unique: forall v p1 p2, valid_path g (v, p1) -> valid_path g (v, p2) -> length p1 <= length p2 -> exists p3, p2 = p1 ++ p3.
proof: Proof. intros. revert p1 H H1. apply (rev_ind (fun p1 => (valid_path g (v, p1) -> length p1 <= length p2 -> exists p3 : list Edge, p2 = p1 ++ p3))); intros. - exists p2. simpl. auto. - pose proof H1. apply valid_path_app in H3. destruct H3 as [? _]. apply H in H3. + destruct H3 as [p4 ?]. destruct p4. * rewrite app_nil_r in H3. subst p2. rewrite app_length in H2. simpl in H2. exfalso; intuition. * exists p4. subst p2. rewrite <- app_assoc. simpl. f_equal. f_equal. clear H H2. pose proof H1. pose proof H0. apply pfoot_split in H. apply pfoot_split in H2. assert (strong_evalid g x) by (apply (valid_path_strong_evalid _ _ _ _ H1); rewrite in_app_iff; right; intuition). destruct H3 as [? _]. assert (strong_evalid g e) by (apply (valid_path_strong_evalid _ _ _ _ H0); rewrite in_app_iff; right; intuition). destruct H4 as [? [? _]]. rewrite <- H2 in H5. assert (x = out_edge (pfoot g (v, l))) by (apply only_one_edge; auto). assert (e = out_edge (pfoot g (v, l))) by (apply only_one_edge; auto). rewrite <- H6 in H7. auto. + rewrite app_length in H2. simpl in H2. intuition. Qed.
imports: Coq.Classes.Morphisms Coq.micromega.Lia Coq.Logic.FunctionalExtensionality CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.EnumEnsembles CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.MathGraph CertiGraph.graph.FiniteGraph