Moved two lemmas out of insertimplappears
Removed several admits and proved find_subtree_leaf_impl_ge_first_key