---

Step * 1 1 of Lemma div_unique


1. a : ℕ
2. n : ℕ+
3. p : ℕ
4. q : ℕ
5. (n * p) ≤ a
6. a < n * (p + 1)
7. (n * q) ≤ a
8. a < n * (q + 1)
⊢ p = q ∈ ℤ
BY
{ ((FwdThruLemma `lt_transitivity_2` [5;8] THEN Auto)
   THEN (FwdThruLemma `lt_transitivity_2` [6;7] THEN Auto)
   THEN (FwdThruLemma `mul_cancel_in_lt` [9] THEN Auto)
   THEN FwdThruLemma `mul_cancel_in_lt` [10]
   THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbN{}
2.  n  :  \mBbbN{}\msupplus{}
3.  p  :  \mBbbN{}
4.  q  :  \mBbbN{}
5.  (n  *  p)  \mleq{}  a
6.  a  <  n  *  (p  +  1)
7.  (n  *  q)  \mleq{}  a
8.  a  <  n  *  (q  +  1)
\mvdash{}  p  =  q


By

---

Latex:
((FwdThruLemma  `lt\_transitivity\_2`  [5;8]  THEN  Auto)
  THEN  (FwdThruLemma  `lt\_transitivity\_2`  [6;7]  THEN  Auto)
  THEN  (FwdThruLemma  `mul\_cancel\_in\_lt`  [9]  THEN  Auto)
  THEN  FwdThruLemma  `mul\_cancel\_in\_lt`  [10]
  THEN  Auto)

---

Home Index