proposition: Lemma path_ends_In_path_src: forall (g: Gph) a b a2b, path_ends g a2b a b -> In_path g a a2b.
proof: Proof. intros. left. destruct H. rewrite (surjective_pairing a2b) in H. simpl in H. symmetry; 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