Commit 2022-07-17 04:14 5a6671a7
View on Github →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.