Commit 2025-12-05 23:23 0a1e860c

View on Github →

chore(Order/SuccPred/Basic): use to_dual (#32447) Not everything has been dualized yet. Dualizing theorems about Monotone, Ixx, Order(Bot/Top) still depends on other PRs.

Estimated changes

deleted theorem Order.le_le_succ_iff
deleted theorem Order.le_of_pred_lt
deleted theorem Order.le_pred_iff
deleted theorem Order.le_pred_iff_isMin
deleted theorem Order.le_pred_of_lt
deleted theorem Order.min_of_le_pred
deleted def Order.pred
deleted theorem Order.pred_eq_iff_isMin
deleted theorem Order.pred_eq_pred_iff
deleted theorem Order.pred_injective
deleted theorem Order.pred_iterate_le
deleted theorem Order.pred_le
deleted theorem Order.pred_le_le_iff
deleted theorem Order.pred_le_pred
deleted theorem Order.pred_le_pred_iff
deleted theorem Order.pred_le_pred_of_le
deleted theorem Order.pred_lt
deleted theorem Order.pred_lt_iff
deleted theorem Order.pred_lt_of_le
deleted theorem Order.pred_lt_pred
deleted theorem Order.pred_lt_pred_iff
deleted theorem Order.pred_ne_pred_iff
modified theorem Order.succ_le_succ_iff
modified theorem Order.succ_lt_succ
modified theorem Order.succ_lt_succ_iff