case inl
F : Type ?u.94914
α : Type u_1
β : Type ?u.94920
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : a ≤ 0
⊢ ⌊a / ↑n⌋₊ = ⌊a⌋₊ / n

case inr
F : Type ?u.94914
α : Type u_1
β : Type ?u.94920
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : 0 ≤ a
⊢ ⌊a / ↑n⌋₊ = ⌊a⌋₊ / n
F : Type ?u.94914
α : Type u_1
β : Type ?u.94920
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
⊢ ⌊a / ↑n⌋₊ = ⌊a⌋₊ / n
cases' le_total a 0 with ha ha
case inr.inl
F : Type ?u.94914
α : Type u_1
β : Type ?u.94920
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
ha : 0 ≤ a
⊢ ⌊a / ↑0⌋₊ = ⌊a⌋₊ / 0

case inr.inr
F : Type ?u.94914
α : Type u_1
β : Type ?u.94920
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : 0 ≤ a
hn : n > 0
⊢ ⌊a / ↑n⌋₊ = ⌊a⌋₊ / n
case inr
F : Type ?u.94914
α : Type u_1
β : Type ?u.94920
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : 0 ≤ a
⊢ ⌊a / ↑n⌋₊ = ⌊a⌋₊ / n
obtain rfl | hn := n.eq_zero_or_pos
case inr.inr.refine'_1
F : Type ?u.94914
α : Type u_1
β : Type ?u.94920
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : 0 ≤ a
hn : n > 0
⊢ 0 ≤ a / ↑n

case inr.inr.refine'_2
F : Type ?u.94914
α : Type u_1
β : Type ?u.94920
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : 0 ≤ a
hn : n > 0
⊢ ↑(⌊a⌋₊ / n) ≤ a / ↑n ∧ a / ↑n < ↑(⌊a⌋₊ / n) + 1
case inr.inr
F : Type ?u.94914
α : Type u_1
β : Type ?u.94920
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : 0 ≤ a
hn : n > 0
⊢ ⌊a / ↑n⌋₊ = ⌊a⌋₊ / n
refine' (floor_eq_iff _).2 _
case inr.inr.refine'_2.left
F : Type ?u.94914
α : Type u_1
β : Type ?u.94920
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : 0 ≤ a
hn : n > 0
⊢ ↑(⌊a⌋₊ / n) ≤ a / ↑n

case inr.inr.refine'_2.right
F : Type ?u.94914
α : Type u_1
β : Type ?u.94920
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : 0 ≤ a
hn : n > 0
⊢ a / ↑n < ↑(⌊a⌋₊ / n) + 1
case inr.inr.refine'_2
F : Type ?u.94914
α : Type u_1
β : Type ?u.94920
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : 0 ≤ a
hn : n > 0
⊢ ↑(⌊a⌋₊ / n) ≤ a / ↑n ∧ a / ↑n < ↑(⌊a⌋₊ / n) + 1
constructor
case inr.inr.refine'_2.right
F : Type ?u.94914
α : Type u_1
β : Type ?u.94920
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : 0 ≤ a
hn : n > 0
⊢ ⌊a⌋₊ < ⌊a⌋₊ / n * n + n

case inr.inr.refine'_2.right
F : Type ?u.94914
α : Type u_1
β : Type ?u.94920
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : 0 ≤ a
hn : n > 0
⊢ 0 < ↑n
case inr.inr.refine'_2.right
F : Type ?u.94914
α : Type u_1
β : Type ?u.94920
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : 0 ≤ a
hn : n > 0
⊢ a / ↑n < ↑(⌊a⌋₊ / n) + 1
rw [div_lt_iff, add_mul, one_mul, ← cast_mul, ← cast_add, ← floor_lt ha]
case inl
F : Type ?u.94914
α : Type u_1
β : Type ?u.94920
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : a ≤ 0
⊢ 0 = 0 / n

case inl
F : Type ?u.94914
α : Type u_1
β : Type ?u.94920
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : a ≤ 0
⊢ a / ↑n ≤ 0
case inl
F : Type ?u.94914
α : Type u_1
β : Type ?u.94920
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : a ≤ 0
⊢ ⌊a / ↑n⌋₊ = ⌊a⌋₊ / n
rw [floor_of_nonpos, floor_of_nonpos ha]
no goals
case inl
F : Type ?u.94914
α : Type u_1
β : Type ?u.94920
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : a ≤ 0
⊢ a / ↑n ≤ 0
apply div_nonpos_of_nonpos_of_nonneg ha n.cast_nonneg
no goals
case inl
F : Type ?u.94914
α : Type u_1
β : Type ?u.94920
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : a ≤ 0
⊢ 0 = 0 / n
simp
no goals
case inr.inl
F : Type ?u.94914
α : Type u_1
β : Type ?u.94920
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
ha : 0 ≤ a
⊢ ⌊a / ↑0⌋₊ = ⌊a⌋₊ / 0
rw [cast_zero, div_zero, Nat.div_zero, floor_zero]
no goals
case inr.inr.refine'_1
F : Type ?u.94914
α : Type u_1
β : Type ?u.94920
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : 0 ≤ a
hn : n > 0
⊢ 0 ≤ a / ↑n
exact div_nonneg ha n.cast_nonneg
no goals
case inr.inr.refine'_2.left
F : Type ?u.94914
α : Type u_1
β : Type ?u.94920
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : 0 ≤ a
hn : n > 0
⊢ ↑(⌊a⌋₊ / n) ≤ a / ↑n
exact cast_div_le.trans (div_le_div_of_le_of_nonneg (floor_le ha) n.cast_nonneg)
no goals
case inr.inr.refine'_2.right
F : Type ?u.94914
α : Type u_1
β : Type ?u.94920
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : 0 ≤ a
hn : n > 0
⊢ ⌊a⌋₊ < ⌊a⌋₊ / n * n + n
exact lt_div_mul_add hn
no goals
case inr.inr.refine'_2.right
F : Type ?u.94914
α : Type u_1
β : Type ?u.94920
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : 0 ≤ a
hn : n > 0
⊢ 0 < ↑n
exact cast_pos.2 hn