---

Step * of Lemma add-mul-special

∀[x:ℤ]. ∀[y:Top].  (x + (y * x) ~ (1 + y) * x)
BY
{ ((UnivCD THENA Auto) THEN (RWW "mul-distributes-right one-mul" 0 THENA Trivial) THEN SqReflexive) }

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (RWW  "mul-distributes-right  one-mul"  0  THENA  Trivial)  THEN  SqReflexive)

---

Home Index