let N, M be ExtNat; :: thesis: N <= N + M
0 + N <= M + N by XXREAL_3:35;
hence N <= N + M by XXREAL_3:4; :: thesis: verum