proposition: Lemma edgeless_vert_rep: forall v, 0 <= v < size -> (@vert_to_list size edgeless_graph' eformat v) = repeat inf (Z.to_nat size).
proof: Proof. unfold vert_to_list; intros. rewrite map_map. apply list_eq_Znth. + rewrite Zlength_map, nat_inc_list_Zlength, Zlength_repeat'; auto. + intros. rewrite Zlength_map, nat_inc_list_Zlength, Z2Nat.id in H0. 2: lia. rewrite Znth_repeat_inrange by auto. rewrite Znth_map, nat_inc_list_i. simpl; auto. rewrite Z2Nat.id; lia. rewrite nat_inc_list_Zlength. rewrite Z2Nat.id; lia. Qed.
imports: VST.floyd.proofauto CertiGraph.graph.graph_model CertiGraph.graph.MathUAdjMatGraph CertiGraph.graph.SpaceAdjMatGraph1 CertiGraph.lib.List_ext