Commit 2022-07-31 20:14 9bb1256d
View on Github →feat(order/succ_pred/basic): a ≤ succ ⊥ ↔ a = ⊥ ∨ a = succ ⊥ and related (#15567)
We use these new results to golf down the ordinal API.
feat(order/succ_pred/basic): a ≤ succ ⊥ ↔ a = ⊥ ∨ a = succ ⊥ and related (#15567)
We use these new results to golf down the ordinal API.