[math-fun] An interesting definite integral?