---

Step * 3 of Lemma comparison-linear


1. [T] : Type
2. cmp : comparison(T)
3. x : cmp-type(T;cmp)
⊢ ∀y:cmp-type(T;cmp). (cmp-le(cmp;x;y) ∨ cmp-le(cmp;y;x))
BY
{ TACTIC:(Auto
          THEN (Decide cmp-le(cmp;x;y)⋅ THEN Auto)
          THEN Decide cmp-le(cmp;y;x)⋅
          THEN Auto
          THEN Assert ⌜0 = 1 ∈ ℤ⌝⋅
          THEN Auto) }

1
.....assertion..... 
1. T : Type
2. cmp : comparison(T)
3. x : cmp-type(T;cmp)
4. y : cmp-type(T;cmp)
5. ¬cmp-le(cmp;x;y)
6. ¬cmp-le(cmp;y;x)
⊢ 0 = 1 ∈ ℤ

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  cmp  :  comparison(T)
3.  x  :  cmp-type(T;cmp)
\mvdash{}  \mforall{}y:cmp-type(T;cmp).  (cmp-le(cmp;x;y)  \mvee{}  cmp-le(cmp;y;x))


By

---

Latex:
TACTIC:(Auto
                THEN  (Decide  cmp-le(cmp;x;y)\mcdot{}  THEN  Auto)
                THEN  Decide  cmp-le(cmp;y;x)\mcdot{}
                THEN  Auto
                THEN  Assert  \mkleeneopen{}0  =  1\mkleeneclose{}\mcdot{}
                THEN  Auto)

---

Home Index