---

Step * 2 of Lemma not-equal-2


1. x : ℤ@i
2. y : ℤ@i
3. ((1 + x) ≤ y) ∨ ((1 + y) ≤ x)
⊢ ¬(x = y ∈ ℤ)
BY
{ (D -1
   THEN (D 0 THENA Auto)
   THEN HypSubst' (-1) (-2)
   THEN Thin (-1)
   THEN (FLemma `le-add-cancel` [-1] THENA Auto)
   THEN TrivialArith) }

---

Latex:

---

Latex:

1.  x  :  \mBbbZ{}@i
2.  y  :  \mBbbZ{}@i
3.  ((1  +  x)  \mleq{}  y)  \mvee{}  ((1  +  y)  \mleq{}  x)
\mvdash{}  \mneg{}(x  =  y)


By

---

Latex:
(D  -1
  THEN  (D  0  THENA  Auto)
  THEN  HypSubst'  (-1)  (-2)
  THEN  Thin  (-1)
  THEN  (FLemma  `le-add-cancel`  [-1]  THENA  Auto)
  THEN  TrivialArith)

---

Home Index