proposition: Lemma reachable_same_or_edge: forall x y, vvalid G x -> reachable G x y <-> x = y \/ exists z, edge G x z /\ x <> z /\ reachable G z y.
proof: Proof. intros. split; intros. - apply reachable_ind; auto. - destruct H0. + subst y. apply reachable_refl. auto. + destruct H0 as [z [? [? ?]]]. apply edge_reachable with z; auto. Qed.
imports: Coq.Logic.ProofIrrelevance CertiGraph.lib.Ensembles_ext Coq.Lists.List Coq.Classes.Morphisms CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.find_not_in CertiGraph.graph.path_lemmas