α : Type ?u.648739
β : Type ?u.648742
n d k N : ℕ
x : Fin n → ℕ
⊢ 8 * 2 ≤ (8 - 2) * exp 1

α : Type ?u.648739
β : Type ?u.648742
n d k N : ℕ
x : Fin n → ℕ
⊢ 0 < 1 - 2 / exp 1
α : Type ?u.648739
β : Type ?u.648742
n d k N : ℕ
x : Fin n → ℕ
⊢ 2 / (1 - 2 / exp 1) ≤ 8
rw [div_le_iff, mul_sub, mul_one, mul_div_assoc', le_sub_comm, div_le_iff (exp_pos _)]
no goals
α : Type ?u.648739
β : Type ?u.648742
n d k N : ℕ
x : Fin n → ℕ
⊢ 0 < 1 - 2 / exp 1
rw [sub_pos, div_lt_one] <;> exact exp_one_gt_d9.trans' (by norm_num)
α : Type ?u.648739
β : Type ?u.648742
n d k N : ℕ
x : Fin n → ℕ
this : 16 < 6 * 2.7182818283
⊢ 8 * 2 ≤ (8 - 2) * exp 1
α : Type ?u.648739
β : Type ?u.648742
n d k N : ℕ
x : Fin n → ℕ
⊢ 8 * 2 ≤ (8 - 2) * exp 1
have : 16 < 6 * (2.7182818283 : ℝ) := by norm_num
no goals
α : Type ?u.648739
β : Type ?u.648742
n d k N : ℕ
x : Fin n → ℕ
this : 16 < 6 * 2.7182818283
⊢ 8 * 2 ≤ (8 - 2) * exp 1
linarith [exp_one_gt_d9]
no goals
α : Type ?u.648739
β : Type ?u.648742
n d k N : ℕ
x : Fin n → ℕ
⊢ 16 < 6 * 2.7182818283
norm_num
no goals
α : Type ?u.648739
β : Type ?u.648742
n d k N : ℕ
x : Fin n → ℕ
⊢ 0 < 2.7182818283
norm_num