---

Step * of Lemma radd_functionality_wrt_rless2

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

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

---

Latex:

---

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


By

---

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

---

Home Index