proposition: Lemma Zright_child_repr: forall i, 0 <= i -> Int.repr (Zright_child i) = Int.mul (Int.repr 2) (Int.add (Int.repr i) Int.one).
proof: Proof. intros. rewrite Zright_child_unfold. rewrite <- add_repr. rewrite Zleft_child_repr; trivial. rewrite Int.add_assoc. change (Int.add Int.one (Int.repr 1)) with (Int.repr 2). rewrite Int.mul_add_distr_r. reflexivity. Qed.
imports: VST.floyd.proofauto CertiGraph.binheap.binary_heap_model