Completed (insertion at least) AVL implementation, passes the totality checker

I kept the proofs for the rebalance functions just as examples.