proposition: Lemma adde_numE: ~ evalid g (u,v) -> numE EdgeListGG_adde = numE g + 1.
proof: Proof. intros. unfold numE. pose proof (adde_EList1_new H). replace (Zlength (EList EdgeListGG_adde)) with (Zlength ((u,v)::EList g)). apply Zlength_cons. 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