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