---

Step * 1 of Lemma rneq-if-rabs


1. x : ℝ
2. y : ℝ
3. n : ℕ+
4. 4 < |x - y| n
⊢ x ≠ y
BY
{ UseWitness ⌜eval m = 4 * n in
              if ((x m) + 4) < (y m)  then inl m  else (inr m )⌝⋅ }

1
1. x : ℝ
2. y : ℝ
3. n : ℕ+
4. 4 < |x - y| n
⊢ eval m = 4 * n in
  if ((x m) + 4) < (y m)  then inl m  else (inr m ) ∈ x ≠ y

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  y  :  \mBbbR{}
3.  n  :  \mBbbN{}\msupplus{}
4.  4  <  |x  -  y|  n
\mvdash{}  x  \mneq{}  y


By

---

Latex:
UseWitness  \mkleeneopen{}eval  m  =  4  *  n  in
                        if  ((x  m)  +  4)  <  (y  m)    then  inl  m    else  (inr  m  )\mkleeneclose{}\mcdot{}

---

Home Index