F : Type ?u.161267
α : Type u_1
β : Type ?u.161273
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
⊢ 0 ≤ fract a ∧ fract a < 1
F : Type ?u.161267
α : Type u_1
β : Type ?u.161273
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
⊢ ⌊fract a⌋ = 0
rw [floor_eq_iff, Int.cast_zero, zero_add]
no goals
F : Type ?u.161267
α : Type u_1
β : Type ?u.161273
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
⊢ 0 ≤ fract a ∧ fract a < 1
exact ⟨fract_nonneg _, fract_lt_one _⟩