case inl
F : Type ?u.83262
α : Type u_1
β : Type ?u.83268
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : FloorSemiring α
a✝ : α
n✝ : ℕ
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ExistsAddOfLE α
a : α
n : ℕ
ha : a ≤ 0
⊢ ⌊a - ↑n⌋₊ = ⌊a⌋₊ - n

case inr
F : Type ?u.83262
α : Type u_1
β : Type ?u.83268
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : FloorSemiring α
a✝ : α
n✝ : ℕ
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ExistsAddOfLE α
a : α
n : ℕ
ha : 0 ≤ a
⊢ ⌊a - ↑n⌋₊ = ⌊a⌋₊ - n
F : Type ?u.83262
α : Type u_1
β : Type ?u.83268
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : FloorSemiring α
a✝ : α
n✝ : ℕ
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ExistsAddOfLE α
a : α
n : ℕ
⊢ ⌊a - ↑n⌋₊ = ⌊a⌋₊ - n
obtain ha | ha := le_total a 0
case inr.inl
F : Type ?u.83262
α : Type u_1
β : Type ?u.83268
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : FloorSemiring α
a✝ : α
n✝ : ℕ
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ExistsAddOfLE α
a : α
n : ℕ
ha : 0 ≤ a
h : a ≤ ↑n
⊢ ⌊a - ↑n⌋₊ = ⌊a⌋₊ - n

case inr.inr
F : Type ?u.83262
α : Type u_1
β : Type ?u.83268
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : FloorSemiring α
a✝ : α
n✝ : ℕ
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ExistsAddOfLE α
a : α
n : ℕ
ha : 0 ≤ a
h : ↑n ≤ a
⊢ ⌊a - ↑n⌋₊ = ⌊a⌋₊ - n
case inr
F : Type ?u.83262
α : Type u_1
β : Type ?u.83268
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : FloorSemiring α
a✝ : α
n✝ : ℕ
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ExistsAddOfLE α
a : α
n : ℕ
ha : 0 ≤ a
⊢ ⌊a - ↑n⌋₊ = ⌊a⌋₊ - n
cases' le_total a n with h h
no goals
case inl
F : Type ?u.83262
α : Type u_1
β : Type ?u.83268
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : FloorSemiring α
a✝ : α
n✝ : ℕ
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ExistsAddOfLE α
a : α
n : ℕ
ha : a ≤ 0
⊢ ⌊a - ↑n⌋₊ = ⌊a⌋₊ - n
rw [floor_of_nonpos ha, floor_of_nonpos (tsub_nonpos_of_le (ha.trans n.cast_nonneg)), zero_tsub]
case inr.inl
F : Type ?u.83262
α : Type u_1
β : Type ?u.83268
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : FloorSemiring α
a✝ : α
n✝ : ℕ
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ExistsAddOfLE α
a : α
n : ℕ
ha : 0 ≤ a
h : a ≤ ↑n
⊢ ⌊a⌋₊ ≤ n
case inr.inl
F : Type ?u.83262
α : Type u_1
β : Type ?u.83268
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : FloorSemiring α
a✝ : α
n✝ : ℕ
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ExistsAddOfLE α
a : α
n : ℕ
ha : 0 ≤ a
h : a ≤ ↑n
⊢ ⌊a - ↑n⌋₊ = ⌊a⌋₊ - n
rw [floor_of_nonpos (tsub_nonpos_of_le h), eq_comm, tsub_eq_zero_iff_le]
no goals
case inr.inl
F : Type ?u.83262
α : Type u_1
β : Type ?u.83268
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : FloorSemiring α
a✝ : α
n✝ : ℕ
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ExistsAddOfLE α
a : α
n : ℕ
ha : 0 ≤ a
h : a ≤ ↑n
⊢ ⌊a⌋₊ ≤ n
exact Nat.cast_le.1 ((Nat.floor_le ha).trans h)
F : Type ?u.83262
α : Type u_1
β : Type ?u.83268
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : FloorSemiring α
a✝ : α
n✝ : ℕ
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ExistsAddOfLE α
a : α
n : ℕ
ha : 0 ≤ a
h : ↑n ≤ a
⊢ 0 ≤ a - ↑n
case inr.inr
F : Type ?u.83262
α : Type u_1
β : Type ?u.83268
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : FloorSemiring α
a✝ : α
n✝ : ℕ
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ExistsAddOfLE α
a : α
n : ℕ
ha : 0 ≤ a
h : ↑n ≤ a
⊢ ⌊a - ↑n⌋₊ = ⌊a⌋₊ - n
rw [eq_tsub_iff_add_eq_of_le (le_floor h), ← floor_add_nat _, tsub_add_cancel_of_le h]
no goals
F : Type ?u.83262
α : Type u_1
β : Type ?u.83268
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : FloorSemiring α
a✝ : α
n✝ : ℕ
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ExistsAddOfLE α
a : α
n : ℕ
ha : 0 ≤ a
h : ↑n ≤ a
⊢ 0 ≤ a - ↑n
exact le_tsub_of_add_le_left ((add_zero _).trans_le h)