Commit 2021-09-14 15:08 6a6b0a56

View on Github →

chore(order/pilex): use *_order_of_*TO from order.rel_classes (#9129) This changes definitional equality for ≤ on pilex from x < y ∨ x = y to x = y ∨ x < y.

Estimated changes

Modified src/order/pilex.lean

added theorem pilex.le_of_forall_le

Modified src/order/rel_classes.lean

modified def partial_order_of_SO