rw [Int.floor_neg] at i_le_floor_neg_c
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i < c
neg_c_lt_neg_i : -↑i > -c
i_le_floor_neg_c : -i ≥ ⌊-c⌋ + 1
⊢ i ≤ ⌈c⌉ - 1
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i < c
neg_c_lt_neg_i : -↑i > -c
i_le_floor_neg_c : -i ≥ -⌈c⌉ + 1
⊢ i ≤ ⌈c⌉ - 1