proposition: Lemma spanning_tree_inj: forall g1 root g2, spanning_tree g1 root g2 <-> (marked_reachable g1 root g2 /\ SIMPLE_SPANNING_TREE.spanning_tree g1 root (unmarked g1) g2).
proof: Proof. intros. split; intro; destruct H; split; auto. + destruct H0 as [? [? ?]]. split; auto. destruct (node_pred_dec (marked g1) root). - split; intros; [|split; intros]. * unfold unmarked in H3. rewrite negateP_spec in H3; exfalso; auto. * apply reachable_by_head_prop in H3; unfold unmarked in H3; rewrite negateP_spec in H3; exfalso; auto. * apply H2; auto. - unfold unmarked in H1 at 1. rewrite negateP_spec in H1. specialize (H1 n). destruct H1; split; intros; auto. + destruct H0 as [? [? [? ?]]]. split; 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