---

Step * 1 1 1 of Lemma choose-inequality1

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

---

Latex:

---

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


By

---

Latex:
(InstLemma  `choose-formula`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]\mcdot{}  THEN  Auto  THEN  Auto')

---

Home Index