---

Step * of Lemma combinations_aux_rem_property

No Annotations
∀[k:ℕ+]. ∀[n,b,m:ℕ].  (combinations_aux_rem(b rem k;n;m;k) = (combinations_aux(b;n;m) rem k) ∈ ℤ)
BY
{ ((D 0 THENA Auto)
   THEN InductionOnNat
   THEN (RecUnfold `combinations_aux_rem` 0 THEN RecUnfold `combinations_aux` 0)
   THEN Reduce 0
   THEN Auto
   THEN ((SplitOnConclITE THEN Try (Complete (Auto))) THEN RepeatFor 3 ((CallByValueReduce 0 THENA Auto)))⋅) }

1
1. k : ℕ+
2. n : ℤ
3. 0 < n
4. ∀[b,m:ℕ].  (combinations_aux_rem(b rem k;n - 1;m;k) = (combinations_aux(b;n - 1;m) rem k) ∈ ℤ)
5. b : ℕ
6. m : ℕ
7. ¬(n = 0 ∈ ℤ)
⊢ combinations_aux_rem((b rem k) * m rem k;n - 1;m - 1;k) = (combinations_aux(b * m;n - 1;m - 1) rem k) ∈ ℤ

---

Latex:

---

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


By

---

Latex:
((D  0  THENA  Auto)
  THEN  InductionOnNat
  THEN  (RecUnfold  `combinations\_aux\_rem`  0  THEN  RecUnfold  `combinations\_aux`  0)
  THEN  Reduce  0
  THEN  Auto
  THEN  ((SplitOnConclITE  THEN  Try  (Complete  (Auto)))
              THEN  RepeatFor  3  ((CallByValueReduce  0  THENA  Auto))
              )\mcdot{})

---

Home Index