---

Step * of Lemma int-ineq-constraint-factor-sym

∀[a:ℤ]. ∀[g:ℕ+]. ∀[xs,L:ℤ List].  uiff(0 ≤ [a / g * L] ⋅ [1 / xs];0 ≤ [a ÷↓ g / L] ⋅ [1 / xs])
BY
{ (InstLemma `int-ineq-constraint-factor` [] THEN RepeatFor 7 (ParallelLast) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a:\mBbbZ{}].  \mforall{}[g:\mBbbN{}\msupplus{}].  \mforall{}[xs,L:\mBbbZ{}  List].    uiff(0  \mleq{}  [a  /  g  *  L]  \mcdot{}  [1  /  xs];0  \mleq{}  [a  \mdiv{}\mdownarrow{}  g  /  L]  \mcdot{}  [1  /  xs])


By

---

Latex:
(InstLemma  `int-ineq-constraint-factor`  []  THEN  RepeatFor  7  (ParallelLast)  THEN  Auto)

---

Home Index