proposition: Lemma step_in_range2: forall (g: AdjMatGG) x x0, valid_path g x -> In x0 (snd x) -> vvalid g (snd x0).
proof: Proof. intros. rewrite (surjective_pairing x) in H. pose proof (valid_path_strong_evalid g _ _ _ H H0). destruct H1 as [? [_ ?]]. 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