theorem NNReal.div_self_eq_ite {x : NNReal} : x / x = if 0 < x then 1 else 0

theorem NNReal.finset_sum_pos_iff {ι : Type u_1} {s : Finset ι} {f : ι → NNReal} : 0 < ∑ x ∈ s, f x ↔ ∃ x ∈ s, 0 < f x

theorem Real.nnnorm_le_nnnorm {x y : ℝ} (hx : 0 ≤ x) (hy : x ≤ y) : ‖x‖₊ ≤ ‖y‖₊

Transfer an inequality over ℝ to one of NNNorms over ℝ≥0.