for N, M, K being ExtNat holds (K + M) + N = K + (M + N) by XXREAL_3:29;