prove many lemmas in binsearch.v
start: binary-heap (binheap.v)