intros i c h
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
⊢ ∀ {i : ℤ} {c : α}, ↑i > c → i ≥ ⌊c⌋ + 1
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i > c
⊢ i ≥ ⌊c⌋ + 1