proposition: Lemma Zlength_default_val_array: forall t size, 0 <= size -> Zlength (default_val (tarray t size)) = size.
proof: Proof. unfold default_val. simpl. intros. rewrite Zlength_Zrepeat; 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