---

Step * of Lemma le-add-cancel

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

1
1. c : ℤ
2. t : ℤ
3. (c + t) ≤ t
⊢ c ≤ 0

2
1. c : ℤ
2. t : ℤ
3. c ≤ 0
⊢ (c + t) ≤ t

---

Latex:

---

Latex:
\mforall{}[c,t:\mBbbZ{}].    uiff((c  +  t)  \mleq{}  t;c  \mleq{}  0)


By

---

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

---

Home Index