---

Step * 1 of Lemma choose-inequality1


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

1
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)
⊢ False

---

Latex:

---

Latex:

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


By

---

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

---

Home Index