---

Step * 1 of Lemma radd-preserves-rless


1. x : ℝ@i
2. y : ℝ@i
3. z : ℝ@i
4. x < y@i
⊢ (z + x) < (z + y)
BY
{ (BLemma `radd_functionality_wrt_rless1` THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}@i
2.  y  :  \mBbbR{}@i
3.  z  :  \mBbbR{}@i
4.  x  <  y@i
\mvdash{}  (z  +  x)  <  (z  +  y)


By

---

Latex:
(BLemma  `radd\_functionality\_wrt\_rless1`  THEN  Auto)

---

Home Index