It is done

Except for the remaining things in the TODO.
I feel like this is as far as I currently want to develop this. It's a toy project, after all.

The heap property has been proven for all functions, and additional properties are proven which show (partially) that the functions are also correct.

As stated in the readme: This is in no way meant to be used in actual code (use the heap from mathlib instead), but if you do, well, I won't stop you.