feat(SetTheory/Ordinal/Arithmetic): a + b ≤ c ↔ ∀ d < b, a + d < c (#19804)
a + b ≤ c ↔ ∀ d < b, a + d < c