Commit 2025-11-15 02:51 7874fc53

View on Github →

chore(Order/Defs): golf multiple lemmas in LinearOrder using grind (#30897)

Estimated changes

modified theorem le_max_left
modified theorem le_max_right
modified theorem le_min
modified theorem lt_or_gt_of_ne
modified theorem lt_trichotomy
modified theorem max_assoc
modified theorem max_eq_left
modified theorem max_le
modified theorem max_left_comm
modified theorem max_self
modified theorem min_assoc
modified theorem min_eq_left
modified theorem min_le_left
modified theorem min_le_right
modified theorem min_left_comm
modified theorem min_self