---

Step * of Lemma choose-inequality1

∀n:ℕ. ∀i:ℕn.  (choose(n;i) ≤ (n * choose(n - 1;i)))
BY
{ (Auto
   THEN (SupposeNot THEN Assert ⌜False⌝⋅ THEN Auto)
   THEN Assert ⌜n * choose(n - 1;i) < choose(n;i)⌝⋅
   THEN Auto
   THEN Thin (-2)) }

1
1. n : ℕ
2. i : ℕn
3. n * choose(n - 1;i) < choose(n;i)
⊢ False

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}i:\mBbbN{}n.    (choose(n;i)  \mleq{}  (n  *  choose(n  -  1;i)))


By

---

Latex:
(Auto
  THEN  (SupposeNot  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  Assert  \mkleeneopen{}n  *  choose(n  -  1;i)  <  choose(n;i)\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  Thin  (-2))

---

Home Index