proposition: Lemma insert_perm: forall (g: EdgeListGG) x l, Permutation (x::l) (insert g x l).
proof: Proof. induction l. simpl. apply Permutation_refl. simpl. destruct (Z.leb (elabel g x) (elabel g a)). apply Permutation_refl. apply (Permutation_trans (l':=a::x::l)). apply perm_swap. apply perm_skip. apply IHl. 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