---

Step * 1 1 1 1 1 of Lemma satisfiable-elim-eq-constraints


1. xs : ℤ List
2. v : ℤ List
⊢ (v ⋅ xs = 0 ∈ ℤ) ⇒ (-1 * v ⋅ xs ≥ 0 )
BY
{ (RWO "int-dot-mul-left" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  xs  :  \mBbbZ{}  List
2.  v  :  \mBbbZ{}  List
\mvdash{}  (v  \mcdot{}  xs  =  0)  {}\mRightarrow{}  (-1  *  v  \mcdot{}  xs  \mgeq{}  0  )


By

---

Latex:
(RWO  "int-dot-mul-left"  0  THEN  Auto)

---

Home Index