---

Step * 1 2 of Lemma combination-decomp


1. A : Type
2. n : ℕ+
3. u : A
4. v : A List
5. no_repeats(A;v) ∧ (¬(u ∈ v))
6. (||v|| + 1) = n ∈ ℤ
7. v ∈ {a:A| ¬(a = u ∈ A)}  List
⊢ v ∈ Combination(n - 1;{a:A| ¬(a = u ∈ A)} )
BY
{ xxx(MemTypeCD THEN Auto)xxx }

---

Latex:

---

Latex:

1.  A  :  Type
2.  n  :  \mBbbN{}\msupplus{}
3.  u  :  A
4.  v  :  A  List
5.  no\_repeats(A;v)  \mwedge{}  (\mneg{}(u  \mmember{}  v))
6.  (||v||  +  1)  =  n
7.  v  \mmember{}  \{a:A|  \mneg{}(a  =  u)\}    List
\mvdash{}  v  \mmember{}  Combination(n  -  1;\{a:A|  \mneg{}(a  =  u)\}  )


By

---

Latex:
xxx(MemTypeCD  THEN  Auto)xxx

---

Home Index