proposition: Lemma cmp_linear: forall a b, cmp_rel a b \/ cmp_rel b a.
proof: Proof. intros [[? ?] ?] [[? ?] ?]. unfold cmp_rel, cmp, heap_item_priority; simpl. case_eq (Int.lt p1 p); auto. intro. right. case_eq (Int.lt p p1); auto. intro. exfalso. apply lt_inv in H. apply lt_inv in H0. 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