---

Step * of Lemma less-iff-le

∀x,y:ℤ.  uiff(x < y;(1 + x) ≤ y)
BY
{ TACTIC:((UnivCD THENA Auto) THEN (RepeatFor 2 (D 0) THENA Auto)) }

1
1. x : ℤ@i
2. y : ℤ@i
3. x < y
⊢ (1 + x) ≤ y

2
1. x : ℤ@i
2. y : ℤ@i
3. (1 + x) ≤ y
⊢ x < y

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbZ{}.    uiff(x  <  y;(1  +  x)  \mleq{}  y)


By

---

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

---

Home Index