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

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