---

Step * of Lemma minus-le

∀[n,x:ℤ].  uiff((-n) ≤ x;0 ≤ (x + n))
BY
{ ((UnivCD THENA Auto) THEN (RepeatFor 2 (D 0) THENA Auto)) }

1
1. n : ℤ
2. x : ℤ
3. (-n) ≤ x
⊢ 0 ≤ (x + n)

2
1. n : ℤ
2. x : ℤ
3. 0 ≤ (x + n)
⊢ (-n) ≤ x

---

Latex:

---

Latex:
\mforall{}[n,x:\mBbbZ{}].    uiff((-n)  \mleq{}  x;0  \mleq{}  (x  +  n))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (RepeatFor  2  (D  0)  THENA  Auto))

---

Home Index