proposition: Lemma initial_link_ok: forall size, 0 <= size -> linked_correctly (initial_item_list size) (List_ext.nat_inc_list (Z.to_nat size)).
proof: Proof. split. apply List_ext.nat_inc_list_NoDup. intros. rewrite List_ext.nat_inc_list_Zlength. rewrite Zlength_initial_item_list in H0; trivial. subst loc. unfold initial_item_list. rewrite Znth_map. unfold heap_item_key. simpl. rewrite List_ext.nat_inc_list_i. rewrite List_ext.nat_inc_list_i. 4: rewrite List_ext.nat_inc_list_Zlength. 1,2,3,4: lia. Qed.
imports: RelationClasses VST.floyd.proofauto CertiGraph.lib.List_ext CertiGraph.binheap.binary_heap_pro CertiGraph.binheap.binary_heap_malloc_spec CertiGraph.binheap.binary_heap_model CertiGraph.binheap.binary_heap_Zmodel