F : Type ?u.159767
α : Type u_1
β : Type ?u.159773
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z✝ : ℤ
a : α
z : ℤ
⊢ ↑z - ↑⌊↑z⌋ = 0
F : Type ?u.159767
α : Type u_1
β : Type ?u.159773
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z✝ : ℤ
a : α
z : ℤ
⊢ fract ↑z = 0
unfold fract
F : Type ?u.159767
α : Type u_1
β : Type ?u.159773
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z✝ : ℤ
a : α
z : ℤ
⊢ ↑z - ↑z = 0
F : Type ?u.159767
α : Type u_1
β : Type ?u.159773
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z✝ : ℤ
a : α
z : ℤ
⊢ ↑z - ↑⌊↑z⌋ = 0
rw [floor_intCast]
no goals
F : Type ?u.159767
α : Type u_1
β : Type ?u.159773
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z✝ : ℤ
a : α
z : ℤ
⊢ ↑z - ↑z = 0
exact sub_self _