proposition: Lemma simpl_size_t_item: forall s, 12 * s / 4 = 3 * s.
proof: Proof. intro. change 12 with (3 * 4). rewrite <- Z.mul_assoc. rewrite (Z.mul_comm 4). rewrite Z.mul_assoc. rewrite Z.div_mul; 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