proposition: Lemma graph_to_tree_lower_bound': forall lim, (forall root, let (n, tree) := graph_to_tree lim root in n = 2 * length (leaves tree) - 1) /\ (forall l n trL, n = 2 * sum_of_leaves trL -> let (n', trL') := to_tree_list lim l (n, trL) in n' = 2 * sum_of_leaves trL').
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. 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). assert (0 = 2 * sum_of_leaves nil) by intuition. specialize (H1 H2). 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. unfold sum_of_leaves in H1. intuition. + destruct lim; simpl; auto. destruct l; simpl; auto. assert (lim <= up) by intuition. destruct (IHup _ H1) as [? _]. specialize (H2 v). remember (graph_to_tree lim v). destruct p as [current tr]. destruct (eq_nat_dec current 0). 1: intuition. assert (lim - current <= up) by intuition. destruct (IHup _ H3) as [_ ?]. specialize (H4 l (n + current + 1) (tr :: trL)). assert (n + current + 1 = 2 * sum_of_leaves (tr :: trL)). { unfold sum_of_leaves in *. simpl flat_map. rewrite app_length. clear -H0 H2 n0. intuition. } specialize (H4 H5). remember (to_tree_list (lim - current) l (n + current + 1, tr :: trL)). destruct p as [n' 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