---

Step * 1 of Lemma div_rec_case


1. a : ℕ
2. n : ℕ+
3. a ≥ n 
⊢ (a ÷ n) = (((a - n) ÷ n) + 1) ∈ ℤ
BY
{ ((InstLemma `div_elim` [⌜a⌝;⌜n⌝] THENM InstLemma `div_elim` [⌜a - n⌝;⌜n⌝]) THENA Auto) }

1
1. a : ℕ
2. n : ℕ+
3. a ≥ n 
4. ∃q:ℕ. (Div(a;n;q) ∧ ((a ÷ n) = q ∈ ℤ))
5. ∃q:ℕ. (Div(a - n;n;q) ∧ (((a - n) ÷ n) = q ∈ ℤ))
⊢ (a ÷ n) = (((a - n) ÷ n) + 1) ∈ ℤ

---

Latex:

---

Latex:

1.  a  :  \mBbbN{}
2.  n  :  \mBbbN{}\msupplus{}
3.  a  \mgeq{}  n 
\mvdash{}  (a  \mdiv{}  n)  =  (((a  -  n)  \mdiv{}  n)  +  1)


By

---

Latex:
((InstLemma  `div\_elim`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]  THENM  InstLemma  `div\_elim`  [\mkleeneopen{}a  -  n\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}])  THENA  Auto)

---

Home Index