Theorem: book.irrational.lem_aux_ii (FormalBook/Chapter_08.lean)

State before:
n : ℕ
x : ℝ
h_1 : 0 < x
h_2 : x < 0
⊢ 0 < f_aux n x ∧ f_aux n x < 1 / ↑n.factorial
Tactic:
sorry
State after:
no goals