---

Step * 2 of Lemma mul-commutes


1. ∀x,y:ℤ.  ((x * y) = (y * x) ∈ ℤ)
⊢ ∀[x:ℤ]. ∀[y:Top].  (x * y ~ y * x)
BY
{ TACTIC:(SqReasoning
          THEN Try (((InstHyp [⌜x⌝;⌜y⌝] 1⋅ THENA Trivial) THEN HypSubst' (-1) 0 THEN Auto))
          THEN Try ((FLemma `exception-not-value` [-1] THEN Complete (Auto)))
          THEN OnMaybeHyp 9 (\h. (ExceptionSqequal h
                                  THEN HypSubst' (-1) 0
                                  THEN (RWO "int-mul-exception" 0 THENA Auto)
                                  THEN Reduce 0
                                  THEN Auto))) }

---

Latex:

---

Latex:

1.  \mforall{}x,y:\mBbbZ{}.    ((x  *  y)  =  (y  *  x))
\mvdash{}  \mforall{}[x:\mBbbZ{}].  \mforall{}[y:Top].    (x  *  y  \msim{}  y  *  x)


By

---

Latex:
TACTIC:(SqReasoning
                THEN  Try  (((InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]  1\mcdot{}  THENA  Trivial)  THEN  HypSubst'  (-1)  0  THEN  Auto))
                THEN  Try  ((FLemma  `exception-not-value`  [-1]  THEN  Complete  (Auto)))
                THEN  OnMaybeHyp  9  (\mbackslash{}h.  (ExceptionSqequal  h
                                                                THEN  HypSubst'  (-1)  0
                                                                THEN  (RWO  "int-mul-exception"  0  THENA  Auto)
                                                                THEN  Reduce  0
                                                                THEN  Auto)))

---

Home Index