実数の加法にはどんな性質があるのかを考えます。

加法律は演算の後で順序の性質が保たれることの要請。

0≤x⇒-x≤0

0≤x(仮定)
(-x)+0≤(-x)+x(加法律)
-x≤0(単位元と逆元)
0≤x⇒-x≤0(含意)

xが0以上ならば-xは0以下。

x≤y⇒0≤(-x)+y

x≤y(仮定)
(-x)+x≤(-x)+y(加法律)
0≤(-x)+y(逆元)
x≤y⇒0≤(-x)+y(含意)

y≤x(仮定)
y+(-x)≤x+(-x)(加法律)
y+(-x)≤0(逆元)
y≤x⇒y+(-x)≤0(含意)

どちらも感覚的には自明な気はしますが。一応定義からの導出ができる実数加法の性質です。

x≤y⇒-y≤-x

x≤y(仮定)
x+(-y)≤y+(-y)(加法律)
x+(-y)≤0(逆元)
(-x)+x+(-y)≤0+(-x)(加法律)
0+(-y)≤x(逆元)
-y≤-x(単位元)
x≤y⇒-y≤-x(含意)

任意の元x,yにマイナスをつけるとその大小関係が入れ替わる性質が証明されました。

これも感覚的には自明な性質ですが、年の為に。