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

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.