proposition: Lemma Zleft_child_repr: forall i, 0 <= i -> Int.repr (Zleft_child i) = Int.add (Int.mul (Int.repr 2) (Int.repr i)) Int.one.
proof: Proof. intros. rewrite Zleft_child_unfold; trivial. unfold Int.one. rewrite mul_repr, add_repr. trivial. Qed.
imports: VST.floyd.proofauto CertiGraph.binheap.binary_heap_model