proposition: Lemma Zleft_child_unfold: forall i, 0 <= i -> Zleft_child i = (2 * i) + 1.
proof: Proof. unfold Zleft_child, binary_heap_model.left_child. intros. do 2 rewrite Nat2Z.inj_add. rewrite Z2Nat.id; lia. Qed.
imports: VST.floyd.proofauto CertiGraph.binheap.binary_heap_model