---

Step * 1 of Lemma count-unordered-combinations


1. n : ℕ
2. m : ℕ
3. n < m
4. UnorderedCombination(m;ℕn)
⊢ False
BY
{ (D (-1)
   THEN Auto
   THEN D -2
   THEN ExRepD
   THEN (RevHypSubst (-3) (-1) THENA Auto)
   THEN Unfold `bag-size` -1
   THEN ThinVar `b') }

1
1. n : ℕ
2. m : ℕ
3. n < m
4. L : ℕn List
5. no_repeats(ℕn;L)
6. ||L|| = m ∈ ℤ
⊢ False

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  m  :  \mBbbN{}
3.  n  <  m
4.  UnorderedCombination(m;\mBbbN{}n)
\mvdash{}  False


By

---

Latex:
(D  (-1)
  THEN  Auto
  THEN  D  -2
  THEN  ExRepD
  THEN  (RevHypSubst  (-3)  (-1)  THENA  Auto)
  THEN  Unfold  `bag-size`  -1
  THEN  ThinVar  `b')

---

Home Index