Theorem: trunc.le_one (PrimeNumberTheoremAnd/Sobolev.lean)

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
g : trunc
x : ℝ
⊢ ∀ x ∉ Set.Ioo (-2) 2, 0 ≤ 1 x
Tactic:
simp
State after:
no goals