---

Step * 1 1 1 of Lemma count-combinations


1. m : ℕ
2. a1 : Combination(0;ℕm)
3. a2 : Combination(0;ℕm)
4. 0 = 0 ∈ ℕ1
⊢ a1 = a2 ∈ Combination(0;ℕm)
BY
{ TACTIC:((RepeatFor 2 (D 2) THEN All Reduce THEN Auto') THEN RepeatFor 2 (D 4) THEN All Reduce THEN Auto') }

---

Latex:

---

Latex:

1.  m  :  \mBbbN{}
2.  a1  :  Combination(0;\mBbbN{}m)
3.  a2  :  Combination(0;\mBbbN{}m)
4.  0  =  0
\mvdash{}  a1  =  a2


By

---

Latex:
TACTIC:((RepeatFor  2  (D  2)  THEN  All  Reduce  THEN  Auto')
                THEN  RepeatFor  2  (D  4)
                THEN  All  Reduce
                THEN  Auto')

---

Home Index