Step * of Lemma not-lt

x,y:ℤ.  uiff(¬x < y;y ≤ x)
BY
Auto }

1
1. : ℤ@i
2. : ℤ@i
3. ¬x < y
⊢ y ≤ x

2
1. : ℤ@i
2. : ℤ@i
3. y ≤ x
⊢ ¬x < y


Latex:


Latex:
\mforall{}x,y:\mBbbZ{}.    uiff(\mneg{}x  <  y;y  \mleq{}  x)


By


Latex:
Auto




Home Index