proposition: Lemma adde_EList_rev: forall l, ~ evalid g (u,v) -> Permutation ((u,v)::l) (EList UAdjMatGG_adde) -> Permutation l (EList g).
proof: Proof. intros. apply NoDup_Permutation. apply NoDup_Perm_EList in H0. apply NoDup_cons_1 in H0; auto. apply NoDup_EList. intros; split; intros. assert (In x (EList UAdjMatGG_adde)). apply (Permutation_in (l:=(u,v)::l)). auto. right; auto. apply EList_evalid in H2. apply adde_evalid_or in H2. destruct H2. rewrite EList_evalid; auto. subst x. assert (NoDup ((u,v)::l)). apply NoDup_Perm_EList in H0; auto. apply NoDup_cons_2 in H2. contradiction. destruct (E_EqDec x (u,v)). unfold equiv in e. subst x. apply EList_evalid in H1; contradiction. unfold complement, equiv in c. apply adde_EList_old in H1. apply (Permutation_in (l':=(u,v)::l)) in H1. destruct H1. symmetry in H1; contradiction. auto. apply Permutation_sym; 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