proposition: Lemma spanning_tree_not_reachable_s: forall (g1 : Graph) (root : V) (P: V -> Prop) (g2 : Graph) x y, spanning_tree g1 root P g2 -> (~ g1 |= root ~o~> y satisfying P) -> reachable g2 x y -> g2 |= x ~o~> y satisfying (Complement _ (reachable_by g1 root P)).
proof: Proof. intros. destruct H as [? [? [? ?]]]. destruct H1 as [p ?]. exists p. assert (valid_path g2 p) by (destruct H1 as [_ [? _]]; auto). split; [|split]; auto. + destruct H1; auto. + rewrite (path_prop_equiv _ _ _ H5). intro v; intros. unfold Complement. unfold Ensembles.In. destruct (reachable_by_path_split_in _ _ _ _ _ _ H1 H6) as [p1 [p2 [? [? ?]]]]. apply reachable_by_path_is_reachable in H9. intro. specialize (H4 _ _ H10 H0). auto. Qed.
imports: Coq.Classes.Morphisms CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.EnumEnsembles CertiGraph.lib.List_ext CertiGraph.lib.relation_list CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.subgraph2 CertiGraph.graph.reachable_ind Coq.Logic.Classical