Proved insert_not_split_impl_space_left (and helper-lemma insert_new_into_list_length_gt_length).