proposition: Lemma Zparent_unfold: forall i, 0 < i -> Zparent i = (i - 1) / 2.
proof: Proof. unfold Zparent, parent. intros. rewrite Nat.div2_div, div_Zdiv; auto. rewrite Nat2Z.inj_sub. rewrite Z2Nat.id; lia. lia. Qed.
imports: VST.floyd.proofauto CertiGraph.binheap.binary_heap_model