proposition: Lemma single_unmarked_le: forall g v, graph_has_v g v -> raw_mark (vlabel g v) = false -> vertex_size g v <= unmarked_gen_size g (vgeneration v).
proof: Proof. intros. unfold unmarked_gen_size. remember (filter (fun i : nat => negb (raw_mark (vlabel g (vgeneration v, i)))) (nat_inc_list (number_of_vertices (nth_gen g (vgeneration v))))). assert (In (vindex v) l). { subst l. rewrite filter_In. split. - rewrite nat_inc_list_In_iff. apply (proj2 H). - destruct v; simpl. rewrite negb_true_iff. apply H0. } apply In_Permutation_cons in H1. destruct H1 as [l1 ?]. symmetry in H1. change (vindex v :: l1) with ([vindex v] ++ l1) in H1. transitivity (fold_left (vertex_size_accum g (vgeneration v)) [vindex v] 0). - simpl. destruct v; simpl. apply Z.le_refl. - apply (fold_left_Z_mono (vertex_size_accum g (vgeneration v)) [vindex v] l1 l 0); [intros; apply Z.le_lteq; left; apply vsa_mono | apply vsa_comm | apply H1]. 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