---

Step * 1 1 1 1 of Lemma count-unordered-combinations


1. n : ℕ
2. m : ℕ
3. n < m
4. L : ℕn List
5. no_repeats(ℕn;L)
6. ||L|| = m ∈ ℤ
7. a1 : ℕm
8. a2 : ℕm
9. L[a1] = L[a2] ∈ ℕn
⊢ a1 = a2 ∈ ℕm
BY
{ (SupposeNot THEN (Assert ¬(L[a1] = L[a2] ∈ ℕn) BY Auto)) }

1
1. n : ℕ
2. m : ℕ
3. n < m
4. L : ℕn List
5. no_repeats(ℕn;L)
6. ||L|| = m ∈ ℤ
7. a1 : ℕm
8. a2 : ℕm
9. L[a1] = L[a2] ∈ ℕn
10. ¬(a1 = a2 ∈ ℕm)
11. ¬(L[a1] = L[a2] ∈ ℕn)
⊢ a1 = a2 ∈ ℕm

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  m  :  \mBbbN{}
3.  n  <  m
4.  L  :  \mBbbN{}n  List
5.  no\_repeats(\mBbbN{}n;L)
6.  ||L||  =  m
7.  a1  :  \mBbbN{}m
8.  a2  :  \mBbbN{}m
9.  L[a1]  =  L[a2]
\mvdash{}  a1  =  a2


By

---

Latex:
(SupposeNot  THEN  (Assert  \mneg{}(L[a1]  =  L[a2])  BY  Auto))

---

Home Index