mathlib

6043522e - refactor(order/basic): Change definition of `<` on `α × β` (#10667)

refactor(order/basic): Change definition of `<` on `α × β` (#10667) This prove that `a < b` on `prod` is equivalent to `a.1 < b.1 ∧ a.2 ≤ b.2 ∨ a.1 ≤ b.1 ∧ a.2 < b.2`.