proposition: Lemma vo_lt_gs: forall g v, gen_has_index g (vgeneration v) (vindex v) -> vertex_offset g v < graph_gen_size g (vgeneration v).
proof: Proof. intros. unfold vertex_offset, graph_gen_size. red in H. remember (number_of_vertices (nth_gen g (vgeneration v))). remember (vgeneration v). assert (S (vindex v) <= n)%nat by lia. apply Z.lt_le_trans with (previous_vertices_size g n0 (S (vindex v))). - rewrite pvs_S. apply Zplus_lt_compat_l, svs_gt_one. - apply pvs_mono; assumption. Qed.
imports: Coq.ZArith.ZArith Coq.Program.Basics Coq.micromega.Lia compcert.lib.Integers compcert.common.Values VST.veric.base VST.veric.Clight_lemmas VST.veric.val_lemmas VST.veric.shares VST.msl.seplog VST.msl.shares VST.zlist.sublist VST.floyd.coqlib3 VST.floyd.functional_base VST.floyd.data_at_rec_lemmas VST.zlist.list_solver CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen