---

Step * of Lemma combinations_aux_linear

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

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

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

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[b,m:\mBbbZ{}].    (combinations\_aux(b;n;m)  =  (b  *  combinations\_aux(1;n;m)))


By

---

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

---

Home Index