---

Step * of Lemma comparison-anti

∀[T:Type]. ∀[cmp:comparison(T)]. ∀[x,y:T].  ((cmp x y) = (-(cmp y x)) ∈ ℤ)
BY
{ (Auto THEN D 2 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[cmp:comparison(T)].  \mforall{}[x,y:T].    ((cmp  x  y)  =  (-(cmp  y  x)))


By

---

Latex:
(Auto  THEN  D  2  THEN  Auto)

---

Home Index