---

Step * of Lemma combinations_aux_rem_wf

∀[k:ℕ+]. ∀[n,b,m:ℕ].  (combinations_aux_rem(b;n;m;k) ∈ ℕ)
BY
{ ((D 0 THENA Auto) THEN InductionOnNat THEN RecUnfold `combinations_aux_rem` 0 THEN Reduce 0) }

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

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

---

Latex:

---

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


By

---

Latex:
((D  0  THENA  Auto)  THEN  InductionOnNat  THEN  RecUnfold  `combinations\_aux\_rem`  0  THEN  Reduce  0)

---

Home Index