mathlib3

9c0a5431 - feat(counterexamples/map_floor): `floor`/`ceil` are not preserved under order ring homs (#16198)

feat(counterexamples/map_floor): `floor`/`ceil` are not preserved under order ring homs (#16198) #16025 proves that `⌊f a⌋ = ⌊a⌋` and `⌈f a⌉ = ⌈a⌉` for a **strictly** monotone ring hom `f`. This counterexample shows that this can't be relaxed to `f` monotone.