---

Step * 1 1 1 of Lemma div_rec_case


1. a : ℕ
2. n : ℕ+
3. a ≥ n 
4. p : ℕ
5. Div(a;n;p)
6. (a ÷ n) = p ∈ ℤ
7. q : ℕ
8. Div(a - n;n;q)
9. ((a - n) ÷ n) = q ∈ ℤ
⊢ (a ÷ n) = (((a - n) ÷ n) + 1) ∈ ℤ
BY
{ (SeqOnM [HypSubst 6 0;HypSubst 9 0;OnHyps [9;6] Thin] THENA Auto) }

1
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) ∈ ℤ

---

Latex:

---

Latex:

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


By

---

Latex:
(SeqOnM  [HypSubst  6  0;HypSubst  9  0;OnHyps  [9;6]  Thin]  THENA  Auto)

---

Home Index