---

Step * 1 1 of Lemma combinations-step


1. n : {1...}
2. m : ℕ
3. combinations_aux(1 * m;n - 1;m - 1) = ((1 * m) * combinations_aux(1;n - 1;m - 1)) ∈ ℤ
⊢ eval m2 = m - 1 in combinations_aux(1 * m;n - 1;m2) = (m * combinations_aux(1;n - 1;m - 1)) ∈ ℤ
BY
{ (CallByValueReduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \{1...\}
2.  m  :  \mBbbN{}
3.  combinations\_aux(1  *  m;n  -  1;m  -  1)  =  ((1  *  m)  *  combinations\_aux(1;n  -  1;m  -  1))
\mvdash{}  eval  m2  =  m  -  1  in  combinations\_aux(1  *  m;n  -  1;m2)  =  (m  *  combinations\_aux(1;n  -  1;m  -  1))


By

---

Latex:
(CallByValueReduce  0  THEN  Auto)

---

Home Index