Proof of The Triangle Inequality of a Norm Read in the Type Real

By the triangle inequality of the norm (Norms and Real Normed Spaces (iv)),

$$\lVert u+v\rVert\le\lVert u\rVert+\lVert v\rVert$$

in $\mathbb{R}$. The sum and the order of $\mathrm{Real}$ are those of $\mathbb{R}$ (The Real Numbers as a Type (ii)): the set of $a+b$ is the sum of the sets of $a$ and $b$, that is $a+b=\lVert u\rVert+\lVert v\rVert$, and $c\le a+b$ in $\mathrm{Real}$ holds exactly when the set of $c$ is at most the set of $a+b$ in $\mathbb{R}$. As $c=\lVert u+v\rVert$, the displayed inequality is this statement, so $c\le a+b$.