F : Type ?u.186509
α : Type ?u.186512
β : Type ?u.186515
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a✝ : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b a : k
hb : 0 < b
⊢ a / b < ↑⌊a / b⌋ + 1
F : Type ?u.186509
α : Type ?u.186512
β : Type ?u.186515
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a✝ : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b a : k
hb : 0 < b
⊢ a < b + ↑⌊a / b⌋ * b
rw [← one_add_mul _ b, ← div_lt_iff hb, add_comm]
no goals
F : Type ?u.186509
α : Type ?u.186512
β : Type ?u.186515
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a✝ : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b a : k
hb : 0 < b
⊢ a / b < ↑⌊a / b⌋ + 1
exact lt_floor_add_one _