proposition: Corollary adde_numV: numV EdgeListGG_adde = numV g.
proof: Proof. intros. unfold EdgeListGG_adde. unfold numV. simpl. unfold VList. destruct finiteV. destruct finiteV. simpl. simpl in a. destruct a. destruct a0. assert (Permutation x x0). apply NoDup_Permutation; auto. intros. rewrite H0. rewrite H2. split; auto. apply Permutation_Zlength. auto. Qed.
imports: VST.floyd.proofauto CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen CertiGraph.graph.FiniteGraph CertiGraph.graph.undirected_graph