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