F : Type ?u.235278
α : Type u_1
β : Type ?u.235284
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
ha : fract a ≠ 0
⊢ ↑⌈a⌉ - a = 1 - (a + 1 - ↑⌈a⌉)
F : Type ?u.235278
α : Type u_1
β : Type ?u.235284
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
ha : fract a ≠ 0
⊢ ↑⌈a⌉ - a = 1 - fract a
rw [(or_iff_right ha).mp (fract_eq_zero_or_add_one_sub_ceil a)]
no goals
F : Type ?u.235278
α : Type u_1
β : Type ?u.235284
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
ha : fract a ≠ 0
⊢ ↑⌈a⌉ - a = 1 - (a + 1 - ↑⌈a⌉)
abel