mathlib

5a6671a7 - chore(order/basic): remove two lemmas breaking API boundaries (#15401)

chore(order/basic): remove two lemmas breaking API boundaries (#15401) `order.dual_le` and `order.dual_lt` don't conform to API boundaries, as they abuse the def-eq between `αᵒᵈ` and `α` instead of using `to_dual` or `of_dual` to perform the cast. As such, we remove them.