proposition: Lemma initial_item_list_i: forall i size, 0 <= i < size -> Znth i (initial_item_list size) = (i, Int.zero, Int.zero).
proof: Proof. intros. unfold initial_item_list. rewrite Znth_map. rewrite List_ext.nat_inc_list_i. trivial. 2: rewrite List_ext.nat_inc_list_Zlength. 1,2: 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