Lean → false

Stream: general

[Yaël Dillies]

The recent PR titles allow us to deduce false!

• #16025: floor/ceil are preserved under order ring homs
• #16198: floor/ceil are not preserved under order ring homs

[Kevin Buzzard]

I think if you read the PR descriptions the supposed contradiction disappears

[Mario Carneiro]

although considering you wrote both PRs I'm not sure this should be blamed on lean

[Damiano Testa]

Curiously, #16236 is another counterexample where strict monotonicity implies something is strictly monotone, while monotonicity does not imply the analogous monotonicity result.