mathlib

04559629 - refactor(order/bounds,*): move code around to make `order.bounds` not depend on `complete_lattice` (#1783)

refactor(order/bounds,*): move code around to make `order.bounds` not depend on `complete_lattice` (#1783) * refactor(order/bounds,*): move code around to make `order.bounds` not depend on `complete_lattice` In another PR I'm going to prove more facts in `order/bounds`, then replace many proofs of lemmas about `(c)Sup`/`(c)Inf` with references to lemmas about `is_lub`/`is_glb`. * Move more code to `basic`, rewrite the only remaining proof in `default` * Rename * Add `default.lean`