proposition: Lemma lst_out_edge_only_one: forall x z y, dst g (out_edge x) = z -> reachable g x y -> ~ reachable g z y -> x = y.
proof: Proof. intros. apply reachable_ind.reachable_ind in H0. destruct H0; auto. destruct H0 as [z' [? [? ?]]]. hnf in H0. destruct H0 as [? [? ?]]. rewrite step_spec in H5. destruct H5 as [e [? [? ?]]]. assert (e = out_edge x) by (apply only_one_edge; auto). rewrite <- H8 in H. rewrite H in H7. subst z'. exfalso; auto. 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