---

Step * of Lemma combinations-step

∀[n,m:ℕ].  (C(n;m) ~ if (n =z 0) then 1 else m * C(n - 1;m - 1) fi )
BY
{ xxx((UnivCD THENA Auto) THEN Unfold `combinations` 0)xxx }

1
1. n : ℕ
2. m : ℕ
⊢ combinations_aux(1;n;m) ~ if (n =z 0) then 1 else m * combinations_aux(1;n - 1;m - 1) fi 

---

Latex:

---

Latex:
\mforall{}[n,m:\mBbbN{}].    (C(n;m)  \msim{}  if  (n  =\msubz{}  0)  then  1  else  m  *  C(n  -  1;m  -  1)  fi  )


By

---

Latex:
xxx((UnivCD  THENA  Auto)  THEN  Unfold  `combinations`  0)xxx

---

Home Index