Theorem zorn.zorn_weak_order

refactor(*): switch from order_pair to partial_order

refactor(*): use 'lemma' iff statement is private

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