proposition: Lemma path_ends_valid_src: forall (g: Gph) a b a2b, valid_path g a2b -> path_ends g a2b a b -> vvalid g a.
proof: Proof. intros. apply (valid_path_valid g _ _ H), (path_ends_In_path_src _ _ b); 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