Commit 2026-03-11 14:51 66efb43f

View on Github →

chore(Order/Defs/LinearOrder): avoid grind in very fundamental lemmas (#35841) Some lemmas can be optimized more elegantly, but it requires moving lemmas from other files, so I will do it in a subsequent PR.

Estimated changes

modified theorem le_min
modified theorem le_of_not_gt
modified theorem lt_or_gt_of_ne
modified theorem lt_trichotomy
modified theorem max_def'
modified theorem min_assoc
modified theorem min_def'
modified theorem min_eq_left
modified theorem min_le_left
modified theorem min_le_right
modified theorem min_left_comm
modified theorem min_self