---

Step * of Lemma minus-one-mul-top

∀[x:Top]. (-x ~ (-1) * x)
BY
{ ((UnivCD THENA Auto)
   THEN SqEqualTopToBase
   THEN SqequalSqle
   THEN AssumeHasValue
   THEN Try ((HasValueD (-1) THEN RWO "minus-one-mul<" 0 THEN Auto))
   THEN ExceptionCases (-1)
   THEN Try (Complete (ExceptionNotValue (-1)⋅))
   THEN Try ((ExceptionSqequal (-1) THEN (HypSubst' (-1) 0 THEN Reduce 0) THEN Complete (Auto)))) }

---

Latex:

---

Latex:
\mforall{}[x:Top].  (-x  \msim{}  (-1)  *  x)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  SqEqualTopToBase
  THEN  SqequalSqle
  THEN  AssumeHasValue
  THEN  Try  ((HasValueD  (-1)  THEN  RWO  "minus-one-mul<"  0  THEN  Auto))
  THEN  ExceptionCases  (-1)
  THEN  Try  (Complete  (ExceptionNotValue  (-1)\mcdot{}))
  THEN  Try  ((ExceptionSqequal  (-1)  THEN  (HypSubst'  (-1)  0  THEN  Reduce  0)  THEN  Complete  (Auto))))

---

Home Index