---

Step * of Lemma le-add-cancel-alt

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

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

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

---

Latex:

---

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


By

---

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

---

Home Index