proposition: Lemma UAdjMatGG_VList: forall (g: UAdjMatGG), Permutation (VList g) (nat_inc_list (Z.to_nat size)).
proof: Proof. intros. apply NoDup_Permutation. apply NoDup_VList. apply nat_inc_list_NoDup. intros. rewrite VList_vvalid. rewrite vert_bound. rewrite nat_inc_list_in_iff. rewrite Z_to_nat_max. destruct (Z.lt_trichotomy size 0). rewrite Z.max_r by lia. split; intros; lia. destruct H. rewrite H. unfold Z.max; simpl. split; lia. rewrite Z.max_l by lia. split; 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