---

Step * 1 1 1 1 1 1 of Lemma rless-iff-rpositive

.....truecase..... 
1. r : ℤ@i
2. r < if 0 <z 4 then 4 else -4 fi @i
3. 0 < r
⊢ r ≤ 3
BY
{ (SplitOnHypITE -2  THEN Auto') }

---

Latex:

---

Latex:
.....truecase..... 
1.  r  :  \mBbbZ{}@i
2.  r  <  if  0  <z  4  then  4  else  -4  fi  @i
3.  0  <  r
\mvdash{}  r  \mleq{}  3


By

---

Latex:
(SplitOnHypITE  -2    THEN  Auto')

---

Home Index