α : Type ?u.696433
β : Type ?u.696436
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 2 / (1 - 2 / exp 1) ≤ x
⊢ x / exp 1 ≤ x / 2 - 1
α : Type ?u.696433
β : Type ?u.696436
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 2 / (1 - 2 / exp 1) ≤ x
⊢ x / exp 1 < ↑⌊x / 2⌋₊
apply lt_of_le_of_lt _ (sub_one_lt_floor _)
α : Type ?u.696433
β : Type ?u.696436
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 2 / (1 - 2 / exp 1) ≤ x
this : 0 < 1 - 2 / exp 1
⊢ x / exp 1 ≤ x / 2 - 1
α : Type ?u.696433
β : Type ?u.696436
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 2 / (1 - 2 / exp 1) ≤ x
⊢ x / exp 1 ≤ x / 2 - 1
have : 0 < 1 - 2 / exp 1 := by
  rw [sub_pos, div_lt_one (exp_pos _)]
  exact lt_of_le_of_lt (by norm_num) exp_one_gt_d9
α : Type ?u.696433
β : Type ?u.696436
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 2 / (1 - 2 / exp 1) ≤ x
this : 0 < 1 - 2 / exp 1
⊢ 0 < 2

case hc
α : Type ?u.696433
β : Type ?u.696436
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 2 / (1 - 2 / exp 1) ≤ x
this : 0 < 1 - 2 / exp 1
⊢ 2 ≠ 0
α : Type ?u.696433
β : Type ?u.696436
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 2 / (1 - 2 / exp 1) ≤ x
this : 0 < 1 - 2 / exp 1
⊢ x / exp 1 ≤ x / 2 - 1
rwa [le_sub_comm, div_eq_mul_one_div x, div_eq_mul_one_div x, ← mul_sub, div_sub', ←
  div_eq_mul_one_div, mul_div_assoc', one_le_div, ← div_le_iff this]
α : Type ?u.696433
β : Type ?u.696436
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 2 / (1 - 2 / exp 1) ≤ x
⊢ 2 < exp 1
α : Type ?u.696433
β : Type ?u.696436
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 2 / (1 - 2 / exp 1) ≤ x
⊢ 0 < 1 - 2 / exp 1
rw [sub_pos, div_lt_one (exp_pos _)]
no goals
α : Type ?u.696433
β : Type ?u.696436
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 2 / (1 - 2 / exp 1) ≤ x
⊢ 2 < exp 1
exact lt_of_le_of_lt (by norm_num) exp_one_gt_d9
no goals
α : Type ?u.696433
β : Type ?u.696436
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 2 / (1 - 2 / exp 1) ≤ x
⊢ 2 ≤ 2.7182818283
norm_num
no goals
α : Type ?u.696433
β : Type ?u.696436
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 2 / (1 - 2 / exp 1) ≤ x
this : 0 < 1 - 2 / exp 1
⊢ 0 < 2
exact zero_lt_two
no goals
case hc
α : Type ?u.696433
β : Type ?u.696436
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 2 / (1 - 2 / exp 1) ≤ x
this : 0 < 1 - 2 / exp 1
⊢ 2 ≠ 0
exact two_ne_zero