proposition: Lemma stcte_add: forall g gi i, number_of_vertices gi = O -> safe_to_copy_to_except g i -> safe_to_copy_to_except (lgraph_add_new_gen g gi) i.
proof: Proof. intros. unfold safe_to_copy_to_except in *. intros. rewrite ang_graph_has_gen in H3. destruct H3. - specialize (H0 _ H1 H2 H3). unfold safe_to_copy_gen in *. rewrite <- ang_graph_gen_size_old; assumption. - unfold safe_to_copy_gen. simpl. unfold graph_gen_size. rewrite H3 at 4. rewrite ang_nth_new, H. unfold previous_vertices_size. simpl. destruct n. 1: contradiction. simpl. rewrite Z.sub_0_r. apply nth_gen_size_le_S. 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