proposition: Lemma Zparent_repr: forall i, 0 < i <= Int.max_unsigned -> Int.repr (Zparent i) = Int.divu (Int.repr (i - 1)) (Int.repr 2).
proof: Proof. intros. unfold Int.divu. repeat rewrite Int.unsigned_repr. 2,3: rep_lia. rewrite Zparent_unfold. trivial. lia. Qed.
imports: VST.floyd.proofauto CertiGraph.binheap.binary_heap CertiGraph.binheap.binary_heap_model CertiGraph.binheap.binary_heap_Zmodel RelationClasses