---

Step * 1 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)
⊢ Div(a;n;q + 1)
BY
{ (UnfoldTopAb (-1) THEN UnfoldTopAb 0 THEN D 7 THEN D 0) }

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

2
1. a : ℕ
2. n : ℕ+
3. a ≥ n 
4. p : ℕ
5. Div(a;n;p)
6. q : ℕ
7. (n * q) ≤ (a - n)
8. a - n < n * (q + 1)
⊢ a < n * ((q + 1) + 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{}  Div(a;n;q  +  1)


By

---

Latex:
(UnfoldTopAb  (-1)  THEN  UnfoldTopAb  0  THEN  D  7  THEN  D  0)

---

Home Index