---

Step * 2 1 of Lemma divides_invar_2


1. a : ℤ
2. b : ℤ
3. c : ℤ
4. (-b) = (a * c) ∈ ℤ
⊢ b = (a * (-c)) ∈ ℤ
BY
{ (RWH (IfIsC ⌜b⌝ (RevLemmaC `minus_minus_cancel`)) 0 THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
2.  b  :  \mBbbZ{}
3.  c  :  \mBbbZ{}
4.  (-b)  =  (a  *  c)
\mvdash{}  b  =  (a  *  (-c))


By

---

Latex:
(RWH  (IfIsC  \mkleeneopen{}b\mkleeneclose{}  (RevLemmaC  `minus\_minus\_cancel`))  0  THEN  Auto)

---

Home Index