---

Step * of Lemma int-ineq-constraint-factor

∀[a:ℤ]. ∀[g:ℕ+]. ∀[xs,L:ℤ List].  uiff(0 ≤ [1 / xs] ⋅ [a / g * L];0 ≤ [1 / xs] ⋅ [a ÷↓ g / L])
BY
{ (Auto THEN All Reduce) }

1
1. a : ℤ
2. g : ℕ+
3. xs : ℤ List
4. L : ℤ List
5. 0 ≤ ((1 * a) + xs ⋅ g * L)
⊢ 0 ≤ ((1 * (a ÷↓ g)) + xs ⋅ L)

2
1. a : ℤ
2. g : ℕ+
3. xs : ℤ List
4. L : ℤ List
5. 0 ≤ ((1 * (a ÷↓ g)) + xs ⋅ L)
⊢ 0 ≤ ((1 * a) + xs ⋅ g * L)

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  All  Reduce)

---

Home Index