proposition: Lemma adde_EList_new: ~ evalid g (u,v) -> Permutation ((u,v)::(EList g)) (EList UAdjMatGG_adde).
proof: Proof. intros. apply NoDup_Permutation. apply NoDup_cons. rewrite EList_evalid; auto. apply NoDup_EList. apply NoDup_EList. intros; split; intros. rewrite EList_evalid, adde_evalid_or. destruct H0. right; symmetry; auto. left; rewrite EList_evalid in H0; auto. rewrite EList_evalid, adde_evalid_or in H0. destruct H0. right; rewrite EList_evalid; auto. left; symmetry; auto. Qed.
imports: VST.floyd.proofauto CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.lib.find_lemmas CertiGraph.graph.graph_model CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.undirected_graph CertiGraph.graph.MathAdjMatGraph