Theorem inf_eq_bot_iff_le_compl

chore(order/bounded_order): Golf `disjoint` API (#14194) …

chore(order): fix-ups after #9891 (#10538)

refactor(*): split `order_{top,bot}` from `lattice` hierarchy (#9891) …

feat(order/bounded_lattice): add `is_compl.le_sup_right_iff_inf_left_le` (#10014) …

refactor(*): drop `lattice` namespace (#2166) …

algebra/lattice/filter: cleanup move theorems to appropriate places

construct reals as complete, linear ordered field

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

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