---

Step * 1 1 of Lemma comparison-linear


1. [T] : Type
2. cmp : comparison(T)
3. a : cmp-type(T;cmp)
⊢ 0 ≤ (cmp a a)
BY
{ ((Subst' (cmp a a) = 0 ∈ ℤ 0 THENM Auto)
   THEN QuotientElimForEquality (-1)
   THEN GenConclTerm ⌜a⌝⋅
   THEN Auto
   THEN All Thin) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  cmp  :  comparison(T)
3.  a  :  cmp-type(T;cmp)
\mvdash{}  0  \mleq{}  (cmp  a  a)


By

---

Latex:
((Subst'  (cmp  a  a)  =  0  0  THENM  Auto)
  THEN  QuotientElimForEquality  (-1)
  THEN  GenConclTerm  \mkleeneopen{}a\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  All  Thin)

---

Home Index