Def weak_order_dual

construct reals as complete, linear ordered field

refactor(*): switch from order_pair to partial_order

refactor(*): import content from lean/library/data and library_dev