Commit 2021-12-06 05:02 e726945e

refactor(order/atoms): is_simple_order from is_simple_lattice (#10537) Rename is_simple_lattice to is_simple_order, still stating that every element is either bot or top are, and that it is nontrivial. To state is_simple_order, has_le and bounded_order are required to be defined. This allows for an order where ⊤ ≤ ⊥ (the always true order). Many proofs/statements about is_simple_orders have been generalized to require solely partial_order and not lattice. The statements themselves have not been changed. The is_simple_order.distrib_lattice instance has been downgraded into a def to prevent loops. Helper defs have been added like is_simple_order.preorder (which is true given the has_le bounded_order axioms) is_simple_order.linear_order, and is_simple_order.lattice (which are true when partial_order, implying ⊥ < ⊤.).