mathlib

8ce5da4b - feat(algebra/order/archimedean): a few more lemmas (#9997)

feat(algebra/order/archimedean): a few more lemmas (#9997) Prove that `a + m • b ∈ Ioc c (c + b)` for some `m : ℤ`, and similarly for `Ico`. Also move some lemmas out of a namespace.