---

Step * of Lemma combinations_aux_wf

No Annotations
∀[n,b,m:ℕ].  (combinations_aux(b;n;m) ∈ ℕ)
BY
{ (InductionOnNat THEN RecUnfold `combinations_aux` 0 THEN Reduce 0)⋅ }

1
1. n : ℤ
⊢ ∀[b,m:ℕ].  (b ∈ ℕ)

2
1. n : ℤ
2. 0 < n
3. ∀[b,m:ℕ].  (combinations_aux(b;n - 1;m) ∈ ℕ)
⊢ ∀[b,m:ℕ].
    (if (n =z 0) then b else eval b2 = b * m in eval n2 = n - 1 in eval m2 = m - 1 in   combinations_aux(b2;n2;m2) fi 
     ∈ ℕ)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[n,b,m:\mBbbN{}].    (combinations\_aux(b;n;m)  \mmember{}  \mBbbN{})


By

---

Latex:
(InductionOnNat  THEN  RecUnfold  `combinations\_aux`  0  THEN  Reduce  0)\mcdot{}

---

Home Index