Commit 2019-12-07 13:49 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 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