cases lt_trichotomy i (⌊c⌋ + 1) with
| inl iltc =>
  have ilec := (Int.lt_iff_add_one_le i (⌊c⌋ + 1)).mp iltc
  simp at ilec
  have c_le_floor := Int.floor_le c
  have cast_ilec := le_trans (castLE' ilec) c_le_floor
  have abs := lt_of_le_of_lt cast_ilec h
  simp at abs
| inr h' => cases h' with
            | inl ieqc => exact le_of_eq (Eq.symm ieqc)
            | inr igtc => exact le_of_lt igtc
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i > c
⊢ i ≥ ⌊c⌋ + 1
no goals