---

Step * 2 of Lemma equipollent-multiply


1. a : ℕ
2. b : ℕ
3. p1 : ℕa
4. p2 : ℤ
5. 0 ≤ p2
6. p2 < b
⊢ p2 < (a * b) - p1 * b
BY
{ (((InstLemma `mul_bounds_1a` [⌜p1⌝; ⌜b⌝])⋅ THENM (InstLemma `mul_preserves_le` [⌜p1⌝; ⌜a - 1⌝; ⌜b⌝])⋅) THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbN{}
2.  b  :  \mBbbN{}
3.  p1  :  \mBbbN{}a
4.  p2  :  \mBbbZ{}
5.  0  \mleq{}  p2
6.  p2  <  b
\mvdash{}  p2  <  (a  *  b)  -  p1  *  b


By

---

Latex:
(((InstLemma  `mul\_bounds\_1a`  [\mkleeneopen{}p1\mkleeneclose{};  \mkleeneopen{}b\mkleeneclose{}])\mcdot{}
  THENM  (InstLemma  `mul\_preserves\_le`  [\mkleeneopen{}p1\mkleeneclose{};  \mkleeneopen{}a  -  1\mkleeneclose{};  \mkleeneopen{}b\mkleeneclose{}])\mcdot{}
  )
  THEN  Auto
  )

---

Home Index