---

Step * of Lemma divide-le

∀[a:ℕ+]. ∀[b,x:ℤ].  uiff(b ≤ (a * x);adjust_div(b;a) ≤ x)
BY
{ ((UnivCD THENA Auto) THEN Unfold `adjust_div` 0 THEN AutoSplit THEN Auto) }

1
1. a : ℕ+
2. b : ℤ
3. x : ℤ
4. 0 < b rem a
5. b ≤ (a * x)
⊢ ((b ÷ a) + 1) ≤ x

2
1. a : ℕ+
2. b : ℤ
3. x : ℤ
4. 0 < b rem a
5. ((b ÷ a) + 1) ≤ x
⊢ b ≤ (a * x)

3
1. a : ℕ+
2. b : ℤ
3. ¬0 < b rem a
4. x : ℤ
5. b ≤ (a * x)
⊢ (b ÷ a) ≤ x

4
1. a : ℕ+
2. b : ℤ
3. ¬0 < b rem a
4. x : ℤ
5. (b ÷ a) ≤ x
⊢ b ≤ (a * x)

---

Latex:

---

Latex:
\mforall{}[a:\mBbbN{}\msupplus{}].  \mforall{}[b,x:\mBbbZ{}].    uiff(b  \mleq{}  (a  *  x);adjust\_div(b;a)  \mleq{}  x)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Unfold  `adjust\_div`  0  THEN  AutoSplit  THEN  Auto)

---

Home Index