proposition: Lemma sizeOfEnum_cons: forall root l (X: Enumerable Vertex (reachable_through_set G l)) v s lim current tr, vvalid G root -> is_tree G root -> NoDup (v :: l) -> (forall y, In y (v :: l) -> step G root y /\ vvalid G y) -> vvalid G v -> is_tree G v -> NoDup s -> (forall x, In x s <-> reachable_through_set G (v :: l) x) -> 2 * length s <= S lim -> (current, tr) = graph_to_tree lim v -> current <> 0 -> (forall x, reachable G v x <-> In x (leaves tr)) -> 2 * sizeOfEnum X <= lim - current.
proof: Proof. intros. destruct X as [s' [? ?]]. unfold sizeOfEnum. simpl. unfold Ensembles.In in i. cut (length s' + length s' + current <= lim). 1: intuition. pose proof (graph_to_tree_nodup lim v H3 H4). rewrite <- H8 in H11. simpl in H11. assert (forall x, In x s <-> In x (leaves tr ++ s')) by (intros; rewrite H6, reachable_through_set_eq, in_app_iff, <- H10, i; tauto). assert (NoDup (leaves tr ++ s')). { apply NoDup_app_inv; auto. repeat intro. rewrite <- H10 in H13. rewrite i in H14. destruct H14 as [v' [? ?]]. assert (v' = v) by (apply (is_tree_step_eq root v' v x); auto; [destruct (H2 v'); auto; right | destruct (H2 v); auto; left]; auto). subst. apply NoDup_cons_2 in H1. auto. } assert (Permutation s (leaves tr ++ s')) by (apply NoDup_Permutation; auto). apply Permutation_length in H14. rewrite app_length in H14. pose proof (graph_to_tree_lower_bound lim v). destruct (graph_to_tree lim v) as [current' tr']. inversion H8. subst current' tr'. rewrite H14 in H7. clear -H7 H17 H9. 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