proposition: Lemma edgeless_GG_Permutation: Permutation (VList edgeless_GG) (Zseq size).
proof: Proof. intros. apply NoDup_Permutation. apply NoDup_VList. apply Zseq_NoDup. intros; rewrite Zseq_In. unfold VList; destruct finiteV; simpl. destruct a. rewrite H0. rewrite edgeless_GG_vvalid. split; 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