---

Step * of Lemma choose_wf

∀[n:ℕ]. ∀[i:{0...n}].  (choose(n;i) ∈ ℕ)
BY
{ ((D 0) THENA Auto) }

1
1. n : ℕ
⊢ ∀[i:{0...n}]. (choose(n;i) ∈ ℕ)

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[i:\{0...n\}].    (choose(n;i)  \mmember{}  \mBbbN{})


By

---

Latex:
((D  0)  THENA  Auto)

---

Home Index