proposition: Lemma edge_preserved_rev_foot: forall (P: V -> Prop), (forall x y, reachable G x y -> P x -> P y) -> forall x y, reachable G x y -> ~ P y -> reachable_by G x (Complement _ P) y.
proof: Proof. intros. rewrite reachable_ind_reachable in H0. induction H0. + apply reachable_by_refl; auto. + apply edge_reachable_by with y; auto. rewrite <- reachable_ind_reachable in H2. intro. apply (H x z) in H3; [auto |]. apply edge_reachable with y; 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