---

Step * of Lemma le-add-cancel3

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

1
1. c : ℤ
2. d : ℤ
3. t : ℤ
4. t' : ℤ
5. t = t' ∈ ℤ
6. (c + t) ≤ (d + t')
⊢ c ≤ d

2
1. c : ℤ
2. d : ℤ
3. t : ℤ
4. t' : ℤ
5. t = t' ∈ ℤ
6. c ≤ d
⊢ (c + t) ≤ (d + t')

---

Latex:

---

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


By

---

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

---

Home Index