---

Step * of Lemma le-add-cancel2

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

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

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

---

Latex:

---

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


By

---

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

---

Home Index