---

Step * 1 1 2 2 1 1 of Lemma choose-inequality1


1. n : ℕ
2. i : ℕn
3. n * choose(n - 1;i) < choose(n;i)
4. (n - i) * (n)! < (n)!
⊢ False
BY
{ (InstLemma `mul_preserves_le` [⌜1⌝;⌜n - i⌝;⌜(n)!⌝]⋅ THEN Auto THEN Auto') }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  i  :  \mBbbN{}n
3.  n  *  choose(n  -  1;i)  <  choose(n;i)
4.  (n  -  i)  *  (n)!  <  (n)!
\mvdash{}  False


By

---

Latex:
(InstLemma  `mul\_preserves\_le`  [\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}n  -  i\mkleeneclose{};\mkleeneopen{}(n)!\mkleeneclose{}]\mcdot{}  THEN  Auto  THEN  Auto')

---

Home Index