Description: The ordered power series structure is a totally ordered set. (Contributed by Mario Carneiro, 10-Jan-2015)