---

Step * of Lemma divides-fact

∀m:ℕ. ∀c:{2..m + 1-}.  (c | (m)!)
BY
{ (InductionOnNat
   THEN Auto
   THEN Unfold `fact` 0
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN Fold `fact` 0
   THEN Reduce 0
   THEN SplitOnConclITE
   THEN Auto'
   THEN BLemma `divides_product`
   THEN Auto) }

1
1. m : ℤ
2. [%1] : 0 < m
3. ∀c:{2..(m - 1) + 1-}. (c | (m - 1)!)
4. c : {2..m + 1-}
5. 1 ≤ m
⊢ (c | ((m - 1) + 1)) ∨ (c | (m - 1)!)

---

Latex:

---

Latex:
\mforall{}m:\mBbbN{}.  \mforall{}c:\{2..m  +  1\msupminus{}\}.    (c  |  (m)!)


By

---

Latex:
(InductionOnNat
  THEN  Auto
  THEN  Unfold  `fact`  0
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  Fold  `fact`  0
  THEN  Reduce  0
  THEN  SplitOnConclITE
  THEN  Auto'
  THEN  BLemma  `divides\_product`
  THEN  Auto)

---

Home Index