proposition: Lemma edgeless_to_symm_mat: graph_to_symm_mat edgeless_graph' = repeat (repeat inf (Z.to_nat size)) (Z.to_nat size).
proof: Proof. unfold graph_to_symm_mat, graph_to_mat. 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 H by lia. rewrite Znth_repeat_inrange by lia. rewrite Znth_map. rewrite nat_inc_list_i. apply edgeless_vert_rep; lia. rewrite Z2Nat.id by lia; lia. rewrite nat_inc_list_Zlength, Z2Nat.id; lia. Qed.
imports: VST.floyd.proofauto CertiGraph.graph.graph_model CertiGraph.graph.MathUAdjMatGraph CertiGraph.graph.SpaceAdjMatGraph1 CertiGraph.lib.List_ext