---

Step * 2 1 of Lemma rless-iff-rpositive


1. x : ℝ@i
2. y : ℝ@i
3. n : ℕ+@i
4. 4 < (y - x) n
⊢ x < y
BY
{ (RepUR ``rsub radd rminus accelerate`` -1
   THEN (CallByValueReduce (-1) THENA Auto)
   THEN (RWO "reg-seq-list-add-as-l_sum" (-1) THENA Auto)
   THEN Reduce (-1)
   THEN Mul ⌜4⌝ (-1)⋅
   THEN (RWO "div_rem_sum2" (-1) THENA Auto)) }

1
1. x : ℝ@i
2. y : ℝ@i
3. n : ℕ+@i
4. 4 < ((y (4 * n)) + (-(x (4 * n))) + 0) ÷ 4
5. 4 * 4 < ((y (4 * n)) + (-(x (4 * n))) + 0) - (y (4 * n)) + (-(x (4 * n))) + 0 rem 4
⊢ x < y

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}@i
2.  y  :  \mBbbR{}@i
3.  n  :  \mBbbN{}\msupplus{}@i
4.  4  <  (y  -  x)  n
\mvdash{}  x  <  y


By

---

Latex:
(RepUR  ``rsub  radd  rminus  accelerate``  -1
  THEN  (CallByValueReduce  (-1)  THENA  Auto)
  THEN  (RWO  "reg-seq-list-add-as-l\_sum"  (-1)  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  Mul  \mkleeneopen{}4\mkleeneclose{}  (-1)\mcdot{}
  THEN  (RWO  "div\_rem\_sum2"  (-1)  THENA  Auto))

---

Home Index