---

Step * 1 1 1 1 of Lemma div_rec_case


1. a : ℕ
2. n : ℕ+
3. a ≥ n 
4. p : ℕ
5. Div(a;n;p)
6. q : ℕ
7. Div(a - n;n;q)
⊢ p = (q + 1) ∈ ℤ
BY
{ (Using [`a',⌜a⌝;`n',⌜n⌝] (BackThruLemma `div_unique`) THEN Auto) }

1
1. a : ℕ
2. n : ℕ+
3. a ≥ n 
4. p : ℕ
5. Div(a;n;p)
6. q : ℕ
7. Div(a - n;n;q)
⊢ Div(a;n;q + 1)

---

Latex:

---

Latex:

1.  a  :  \mBbbN{}
2.  n  :  \mBbbN{}\msupplus{}
3.  a  \mgeq{}  n 
4.  p  :  \mBbbN{}
5.  Div(a;n;p)
6.  q  :  \mBbbN{}
7.  Div(a  -  n;n;q)
\mvdash{}  p  =  (q  +  1)


By

---

Latex:
(Using  [`a',\mkleeneopen{}a\mkleeneclose{};`n',\mkleeneopen{}n\mkleeneclose{}]  (BackThruLemma  `div\_unique`)  THEN  Auto)

---

Home Index