proposition: Lemma EST_reverse_out_edges: forall (P: V -> Prop) (g1 g2: Graph) (e: E) (root: V), ~ P root -> out_edges g1 root e -> edge_spanning_tree g1 e P g2 -> forall e', out_edges g2 root e' -> out_edges g1 root e'.
proof: Proof. intros. destruct H1 as [[_ [? _]] | [_ [_ [? [? [_ ?]]]]]]. + pose proof (ppg_out_edges _ _ _ _ _ H H1). rewrite H3; auto. + destruct_eq_dec e' e. - subst. destruct H4; [destruct H2|]; auto. - specialize (H1 _ H5). specialize (H3 _ H5). hnf. destruct H2. subst root; intuition. 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