This amount of nontrivial, yes. Similarly, I'd expect a computer scientist to come up with a proof of correctness for either binary search or merge sort (the out of place variant) in ~30 minutes. It's not particularly difficult.
The number of incorrect binary search algorithms published in the literature over the years would indicate otherwise…
I agree that reasoning about the correctness of a binary search algorithm is an important job skill for a computer scientist. Deriving the tortoise and hare algorithm on the fly, though, is not.
In any case, I didn't say “trivial”. If you can only derive trivial things, then you shouldn't be a computer scientist.