Split \notin into two subgoals dealing with cases less than start and cases greater than end