proposition: Lemma graph_to_tree_zero: forall lim root, fst (graph_to_tree lim root) = 0 -> lim = 0.
proof: Proof. intros. destruct lim. auto. simpl in H. remember (nodup veq_dec (filter not_null_bool (map (dst G) (edge_func G root)))). remember (to_tree_list lim l (0, nil)). destruct p. simpl in H. exfalso; intuition. Qed.
imports: Coq.Arith.Arith CertiGraph.lib.Coqlib CertiGraph.lib.EnumEnsembles CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.subgraph2 CertiGraph.graph.MathGraph CertiGraph.graph.FiniteGraph CertiGraph.graph.reachable_computable Coq.Lists.List