---

Step * of Lemma radd_functionality_wrt_rless1

∀x,y,z,t:ℝ.  (y < t) ⇒ ((x + y) < (z + t)) supposing x ≤ z
BY
{ (Auto THEN (All (RWO "rless-iff-rpositive") THENA Auto) THEN Unfold `rleq` -2) }

1
1. x : ℝ
2. y : ℝ
3. z : ℝ
4. t : ℝ
5. rnonneg(z - x)
6. rpositive(t - y)
⊢ rpositive((z + t) - x + y)

---

Latex:

---

Latex:
\mforall{}x,y,z,t:\mBbbR{}.    (y  <  t)  {}\mRightarrow{}  ((x  +  y)  <  (z  +  t))  supposing  x  \mleq{}  z


By

---

Latex:
(Auto  THEN  (All  (RWO  "rless-iff-rpositive")  THENA  Auto)  THEN  Unfold  `rleq`  -2)

---

Home Index