proposition: Corollary adde_g2wedgelist_2: forall e', (u,v)<>e' -> evalid g e' -> In (elabel g e', e') (graph_to_wedgelist EdgeListGG_adde).
proof: Proof. intros. unfold graph_to_wedgelist. replace (elabel g e', e') with (edge_to_wedge EdgeListGG_adde e'). apply in_map. apply EList_evalid. apply add_edge_preserves_evalid; auto. unfold edge_to_wedge; simpl. unfold update_elabel. unfold equiv_dec. destruct E_EqDec. contradiction. 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