proposition: Lemma In_links_fst_In_path: forall (g: AdjMatGG) step path, In step (snd path) -> In_path g (fst step) path.
proof: Proof. intros. unfold In_path. right. exists step. split; trivial. left. rewrite (edge_src_fst 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