---

Step * 1 1 of Lemma rleq-implies

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

---

Latex:

---

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


By

---

Latex:
(SplitOnHypITE  -2    THEN  Auto)

---

Home Index