F : Type ?u.264762
α : Type u_1
β : Type ?u.264768
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
⊢ fract x ≤ abs (x - ↑z) ∨ 1 - fract x ≤ abs (x - ↑z)
F : Type ?u.264762
α : Type u_1
β : Type ?u.264768
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
⊢ abs (x - ↑(round x)) ≤ abs (x - ↑z)
rw [abs_sub_round_eq_min, min_le_iff]
case inl.h
F : Type ?u.264762
α : Type u_1
β : Type ?u.264768
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : ↑z ≤ x
⊢ fract x ≤ abs (x - ↑z)

case inr.h
F : Type ?u.264762
α : Type u_1
β : Type ?u.264768
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ 1 - fract x ≤ abs (x - ↑z)
F : Type ?u.264762
α : Type u_1
β : Type ?u.264768
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
⊢ fract x ≤ abs (x - ↑z) ∨ 1 - fract x ≤ abs (x - ↑z)
rcases le_or_lt (z : α) x with (hx | hx) <;> [left; right]
case inl.h
F : Type ?u.264762
α : Type u_1
β : Type ?u.264768
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : ↑z ≤ x
⊢ fract x ≤ fract x + (↑⌊x⌋ - ↑z)
case inl.h
F : Type ?u.264762
α : Type u_1
β : Type ?u.264768
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : ↑z ≤ x
⊢ fract x ≤ abs (x - ↑z)
conv_rhs => rw [abs_eq_self.mpr (sub_nonneg.mpr hx), ← fract_add_floor x, add_sub_assoc]
no goals
case inl.h
F : Type ?u.264762
α : Type u_1
β : Type ?u.264768
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : ↑z ≤ x
⊢ fract x ≤ fract x + (↑⌊x⌋ - ↑z)
simpa only [le_add_iff_nonneg_right, sub_nonneg, cast_le] using le_floor.mpr hx
case inr.h
F : Type ?u.264762
α : Type u_1
β : Type ?u.264768
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ 1 - fract x ≤ -(x - ↑z)
case inr.h
F : Type ?u.264762
α : Type u_1
β : Type ?u.264768
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ 1 - fract x ≤ abs (x - ↑z)
rw [abs_eq_neg_self.mpr (sub_neg.mpr hx).le]
case inr.h
F : Type ?u.264762
α : Type u_1
β : Type ?u.264768
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ 1 - fract x ≤ -(fract x + ↑⌊x⌋ - ↑z)
case inr.h
F : Type ?u.264762
α : Type u_1
β : Type ?u.264768
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ 1 - fract x ≤ -(x - ↑z)
conv_rhs => rw [← fract_add_floor x]
case inr.h
F : Type ?u.264762
α : Type u_1
β : Type ?u.264768
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ ↑⌊x⌋ ≤ ↑z - 1
case inr.h
F : Type ?u.264762
α : Type u_1
β : Type ?u.264768
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ 1 - fract x ≤ -(fract x + ↑⌊x⌋ - ↑z)
rw [add_sub_assoc, add_comm, neg_add, neg_sub, le_add_neg_iff_add_le, sub_add_cancel,
  le_sub_comm]
case inr.h
F : Type ?u.264762
α : Type u_1
β : Type ?u.264768
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ ⌊x⌋ ≤ z - 1
case inr.h
F : Type ?u.264762
α : Type u_1
β : Type ?u.264768
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ ↑⌊x⌋ ≤ ↑z - 1
norm_cast
no goals
case inr.h
F : Type ?u.264762
α : Type u_1
β : Type ?u.264768
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ ⌊x⌋ ≤ z - 1
exact floor_le_sub_one_iff.mpr hx