proposition: Lemma graph_to_tree_bound': forall lim, (forall root, fst (graph_to_tree lim root) <= lim) /\ (forall l n trL, fst (to_tree_list lim l (n, trL)) <= lim + n).
proof: Proof. intro lim. remember lim as up. rewrite Hequp. assert (lim <= up) by intuition. clear Hequp. revert lim H. induction up; intros; split; intros. + assert (lim = 0) by intuition. subst. simpl; auto. + assert (lim = 0) by intuition. subst. simpl; auto. + destruct lim; simpl; auto. remember (to_tree_list lim (nodup veq_dec (filter not_null_bool (map (dst G) (edge_func G root)))) (0, nil)). destruct p as [total sub_trees]. simpl. assert (lim <= up) by intuition. destruct (IHup _ H0) as [_ ?]. specialize (H1 (nodup veq_dec (filter not_null_bool (map (dst G) (edge_func G root)))) 0 nil). rewrite <- Heqp in H1. simpl in H1. intuition. + destruct lim; simpl; auto. destruct l; simpl; intuition. remember (graph_to_tree lim v). destruct p as [current tr]. destruct (eq_nat_dec current 0). 1: simpl; intuition. assert (lim <= up) by intuition. destruct (IHup _ H0) as [? _]. specialize (H1 v). rewrite <- Heqp in H1. simpl in H1. assert (lim - current <= up) by intuition. destruct (IHup _ H2) as [_ ?]. specialize (H3 l (n + current + 1) (tr :: trL)). 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