---

Step * of Lemma minus_functionality_wrt_eqmod

∀m,a,a':ℤ.  ((a ≡ a' mod m) ⇒ ((-a) ≡ (-a') mod m))
BY
{ (Auto THEN D -1 THEN With ⌜-c⌝ (D 0)⋅ THEN Auto') }

---

Latex:

---

Latex:
\mforall{}m,a,a':\mBbbZ{}.    ((a  \mequiv{}  a'  mod  m)  {}\mRightarrow{}  ((-a)  \mequiv{}  (-a')  mod  m))


By

---

Latex:
(Auto  THEN  D  -1  THEN  With  \mkleeneopen{}-c\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto')

---

Home Index