cases h' with
| inl ieqc => exact le_of_eq (Eq.symm ieqc)
| inr igtc => exact le_of_lt igtc
case inr
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i > c
h' : i = ⌊c⌋ + 1 ∨ ⌊c⌋ + 1 < i
⊢ i ≥ ⌊c⌋ + 1
no goals