proposition: Lemma listVertices'_In_length_reachable {EV: EqDec V eq} {EE: EqDec E eq}: forall (g: PreGraph V E) root len r (X: EnumCovered V (reachable g root)), length (proj1_sig X) <= len -> NoDup (listVertices' r) -> len <= length r -> (forall v, In v (listVertices' r) -> reachable g root v) -> forall v, reachable g root v -> In v (listVertices' r).
proof: Proof. intros. destruct X as [pl [? ?]]. simpl in H. unfold Ensembles.In in i. assert (incl (listVertices' r) pl) by (hnf; intros; apply H2 in H4; apply i in H4; auto). apply NoDup_Permutation_bis in H4; auto. 1: specialize (i _ H3); apply Permutation_sym in H4; apply Permutation_in with pl; auto. apply NoDup_incl_length in H4; auto. rewrite <- listVertices'_length in H1. intuition. Qed.
imports: Coq.Classes.Morphisms Coq.micromega.Lia Coq.Logic.FunctionalExtensionality CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.EnumEnsembles CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.FiniteGraph