case h.e'_2
F : Type ?u.214801
α : Type u_1
β : Type ?u.214807
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
n : ℕ
⊢ ⌈a - ↑n⌉ = ⌈a - ↑↑n⌉
F : Type ?u.214801
α : Type u_1
β : Type ?u.214807
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
n : ℕ
⊢ ⌈a - ↑n⌉ = ⌈a⌉ - ↑n
convert ceil_sub_int a n using 1
no goals
case h.e'_2
F : Type ?u.214801
α : Type u_1
β : Type ?u.214807
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
n : ℕ
⊢ ⌈a - ↑n⌉ = ⌈a - ↑↑n⌉
simp