proposition: Lemma path_ends_app_cons: forall (g: AdjMatGG) a b c a' a2b, a = a' -> path_ends g (a, a2b) a b -> path_ends g (a, a2b +:: (b, c)) a' c.
proof: Proof. split; trivial. rewrite pfoot_last. rewrite (edge_dst_snd g); trivial. Qed.
imports: Coq.ZArith.BinInt Coq.Classes.EquivDec compcert.lib.Integers CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.FiniteGraph CertiGraph.graph.path_lemmas