Commit 2026-07-27 13:45 d868ca66

feat (Order/Interval/Finset/Floor): Relating membership of an Int or Nat cast in intervals to intervals of floor and ceil functions (#41512) For a FloorRing (resp. FloorSemiring) α, we relate membership of a cast ↑n in an interval of α to membership of the integer (resp. natural number) n in the corresponding interval with floor/ceil endpoints, for instance Int.coe_mem_Ioc_iff : ↑n ∈ Set.Ioc a b ↔ n ∈ Set.Ioc ⌊a⌋ ⌊b⌋. If the right-hand side is finite, we express them as Finset instead.