Commit 2022-12-20 11:07 acffbef0

View on Github →

chore: port order.basic again (#1112) There seem to have been a number of changes since this was ported, and this takes the opportunity to restore the #aligns.

Estimated changes

modified theorem Function.const_le_const
modified theorem Function.const_lt_const
modified theorem LE.le.ge_iff_eq
modified theorem LE.le.gt_iff_ne
modified theorem LE.le.le_iff_eq
modified theorem LE.le.lt_iff_ne
modified theorem LE.le.not_gt_iff_eq
modified theorem LE.le.not_lt_iff_eq
modified theorem PUnit.not_lt
added def StrongLT
modified theorem commutative_of_le
modified theorem le_Prop_eq
added theorem le_of_strongLT
modified theorem le_update_iff
added theorem le_update_self_iff
added theorem lt_of_strongLT
added theorem lt_update_self_iff
modified theorem max_def'
added theorem max_def_lt
modified theorem min_def'
added theorem min_def_lt
modified theorem update_le_iff
added theorem update_le_self_iff
modified theorem update_le_update_iff
added theorem update_lt_self_iff