Proved insert'_overflow_impl_lesser_than_next and adjusted insert'_impl_appears.
Almost finished the insert'_overflow_impl_greater_key proof.
Removed one more admit.
Removed a lot of old junk lemmas.
Merge branch 'master' of github.com:nicolaidahl/BPlusTrees