F : Type ?u.78159
α : Type u_1
β : Type ?u.78165
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
n✝ : ℕ
ha : 0 ≤ a
n b : ℕ
⊢ ↑b ≤ a + ↑n ↔ b ≤ ⌊a⌋₊ + n
F : Type ?u.78159
α : Type u_1
β : Type ?u.78165
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
n✝ : ℕ
ha : 0 ≤ a
n b : ℕ
⊢ b ≤ ⌊a + ↑n⌋₊ ↔ b ≤ ⌊a⌋₊ + n
rw [le_floor_iff (add_nonneg ha n.cast_nonneg)]
case inl
F : Type ?u.78159
α : Type u_1
β : Type ?u.78165
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
n✝ : ℕ
ha : 0 ≤ a
n b : ℕ
hb : n ≤ b
⊢ ↑b ≤ a + ↑n ↔ b ≤ ⌊a⌋₊ + n

case inr
F : Type ?u.78159
α : Type u_1
β : Type ?u.78165
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
n✝ : ℕ
ha : 0 ≤ a
n b : ℕ
hb : b ≤ n
⊢ ↑b ≤ a + ↑n ↔ b ≤ ⌊a⌋₊ + n
F : Type ?u.78159
α : Type u_1
β : Type ?u.78165
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
n✝ : ℕ
ha : 0 ≤ a
n b : ℕ
⊢ ↑b ≤ a + ↑n ↔ b ≤ ⌊a⌋₊ + n
obtain hb | hb := le_total n b
case inl.intro
F : Type ?u.78159
α : Type u_1
β : Type ?u.78165
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
n✝ : ℕ
ha : 0 ≤ a
n d : ℕ
hb : n ≤ n + d
⊢ ↑(n + d) ≤ a + ↑n ↔ n + d ≤ ⌊a⌋₊ + n
case inl
F : Type ?u.78159
α : Type u_1
β : Type ?u.78165
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
n✝ : ℕ
ha : 0 ≤ a
n b : ℕ
hb : n ≤ b
⊢ ↑b ≤ a + ↑n ↔ b ≤ ⌊a⌋₊ + n
obtain ⟨d, rfl⟩ := exists_add_of_le hb
no goals
case inl.intro
F : Type ?u.78159
α : Type u_1
β : Type ?u.78165
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
n✝ : ℕ
ha : 0 ≤ a
n d : ℕ
hb : n ≤ n + d
⊢ ↑(n + d) ≤ a + ↑n ↔ n + d ≤ ⌊a⌋₊ + n
rw [Nat.cast_add, add_comm n, add_comm (n : α), add_le_add_iff_right, add_le_add_iff_right,
  le_floor_iff ha]
case inr.intro
F : Type ?u.78159
α : Type u_1
β : Type ?u.78165
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : 0 ≤ a
b d : ℕ
hb : b ≤ b + d
⊢ ↑b ≤ a + ↑(b + d) ↔ b ≤ ⌊a⌋₊ + (b + d)
case inr
F : Type ?u.78159
α : Type u_1
β : Type ?u.78165
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
n✝ : ℕ
ha : 0 ≤ a
n b : ℕ
hb : b ≤ n
⊢ ↑b ≤ a + ↑n ↔ b ≤ ⌊a⌋₊ + n
obtain ⟨d, rfl⟩ := exists_add_of_le hb
case inr.intro
F : Type ?u.78159
α : Type u_1
β : Type ?u.78165
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : 0 ≤ a
b d : ℕ
hb : b ≤ b + d
⊢ ↑b ≤ ↑b + (a + ↑d) ↔ b ≤ b + (⌊a⌋₊ + d)
case inr.intro
F : Type ?u.78159
α : Type u_1
β : Type ?u.78165
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : 0 ≤ a
b d : ℕ
hb : b ≤ b + d
⊢ ↑b ≤ a + ↑(b + d) ↔ b ≤ ⌊a⌋₊ + (b + d)
rw [Nat.cast_add, add_left_comm _ b, add_left_comm _ (b : α)]
case inr.intro
F : Type ?u.78159
α : Type u_1
β : Type ?u.78165
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : 0 ≤ a
b d : ℕ
hb : b ≤ b + d
⊢ ↑b ≤ ↑b + (a + ↑d)
case inr.intro
F : Type ?u.78159
α : Type u_1
β : Type ?u.78165
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : 0 ≤ a
b d : ℕ
hb : b ≤ b + d
⊢ ↑b ≤ ↑b + (a + ↑d) ↔ b ≤ b + (⌊a⌋₊ + d)
refine' iff_of_true _ le_self_add
no goals
case inr.intro
F : Type ?u.78159
α : Type u_1
β : Type ?u.78165
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : 0 ≤ a
b d : ℕ
hb : b ≤ b + d
⊢ ↑b ≤ ↑b + (a + ↑d)
exact le_add_of_nonneg_right <| ha.trans <| le_add_of_nonneg_right d.cast_nonneg