proposition: Lemma Zlength_initializing_item_list: forall size capacity, 0 <= size < capacity -> Zlength (initializing_item_list size capacity) = capacity.
proof: Proof. unfold initializing_item_list. intros. rewrite Zlength_app, Zlength_map, Zlength_initial_item_list, (Zlength_default_val_array t_item); 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