The Triangle Inequality of a Norm Read in the Type Real

In the setting of Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity and Real Normed, Inner Product and Hilbert Spaces: Notation, with $+$ and $\le$ on the type $\mathrm{Real}$ of The Real Numbers as a Type (i) those of The Real Numbers as a Type (ii); for $q$ in $\mathrm{Real}$ and a set $s$, $q=s$ means that the set of $q$ is $s$.

(i) The triangle inequality in $\mathrm{Real}$. Let $(V,\lVert\cdot\rVert)$ be a real normed space and $u,v\in V$. If $a$, $b$ and $c$ are in $\mathrm{Real}$ with $a=\lVert u\rVert$, $b=\lVert v\rVert$ and $c=\lVert u+v\rVert$, then

$$c\le a+b\quad\text{in }\mathrm{Real}.$$