---

Step * of Lemma divides_subtract

∀x,y,z:ℤ.  ((x | y) ⇒ (x | z) ⇒ (x | (y - z)))
BY
{ ((Unfold `divides` 0 THEN Auto) THEN ExRepD THEN With ⌜c1 - c⌝ (D 0)⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}x,y,z:\mBbbZ{}.    ((x  |  y)  {}\mRightarrow{}  (x  |  z)  {}\mRightarrow{}  (x  |  (y  -  z)))


By

---

Latex:
((Unfold  `divides`  0  THEN  Auto)  THEN  ExRepD  THEN  With  \mkleeneopen{}c1  -  c\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index