```
(def-theorem factorial-of-zero
"0!=1"
(theory h-o-real-arithmetic)
(proof
(
(unfold-single-defined-constant-globally factorial)
(unfold-single-defined-constant-globally prod)
simplify
)))
```

```
(def-compound-macete factorial-reduction
(without-minor-premises
(repeat factorial-out factorial-of-zero)))
```

```(def-script comb-ident-script 0
((unfold-single-defined-constant-globally comb)
(apply-macete-with-minor-premises fractional-expression-manipulation)
(label-node compound)
direct-and-antecedent-inference-strategy
(jump-to-node compound)
(for-nodes
(unsupported-descendents)
(if (matches? "with(t:rr, #(t^[-1]))")
(apply-macete-with-minor-premises definedness-manipulations)
(block
(apply-macete-with-minor-premises factorial-reduction)
simplify)))))
```

```
(def-theorem comb-ident
"forall(k,m:zz,1<=k and k<=m implies comb(1+m,k)=comb(m,k-1)+comb(m,k))"
(theory h-o-real-arithmetic)
(proof
(
(unfold-single-defined-constant-globally comb)
(apply-macete-with-minor-premises fractional-expression-manipulation)
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises definedness-manipulations)
(apply-macete-with-minor-premises definedness-manipulations)
(block (apply-macete-with-minor-premises factorial-reduction) simplify)
)))
```

```
(def-theorem comb-0-value-lemma
"forall(m:zz,0<=m implies comb(m,0)=1)"
(proof
(

(unfold-single-defined-constant (0) comb)
simplify
(unfold-single-defined-constant (0) factorial)
(unfold-single-defined-constant (0) prod)
simplify
))
(theory h-o-real-arithmetic))
```

```
(def-theorem comb-1-value-lemma
"forall(m:zz,1<=m implies comb(m,1)=m)"
(theory h-o-real-arithmetic)
(proof
(
(unfold-single-defined-constant (0) comb)
(apply-macete factorial-out)
simplify
(unfold-single-defined-constant (0) factorial)
(unfold-single-defined-constant (0) prod)
simplify
)))
```

```
(def-theorem comb-m-value-lemma
"forall(m:zz, comb(m,m)=1)"
(theory h-o-real-arithmetic)
(proof
(
(unfold-single-defined-constant (0) comb)
simplify
(unfold-single-defined-constant (0) factorial)
(unfold-single-defined-constant (0) prod)
simplify
)))
```

```
(def-theorem comb-definedness-lemma
"forall(m,k:zz,#(comb(m,k)))"
(theory h-o-real-arithmetic)
(proof
(
insistent-direct-inference
unfold-defined-constants
simplify
))
(usages d-r-convergence))
```

```
(def-theorem comb-integrality-lemma
"forall(m,k:zz,k<=m and 0<=k implies #(comb(m,k),zz))"
(theory h-o-real-arithmetic)
(usages d-r-convergence)
(proof
(
(cut-with-single-formula "forall(m:zz,0<=m implies forall(k,p:zz,0<=k and k<=p and p<=m implies #(comb(p,k),zz)))")
direct-and-antecedent-inference-strategy
(backchain "forall(m:zz,
0<=m
implies
forall(k,p:zz,
0<=k and k<=p and p<=m implies #(comb(p,k),zz)));")
(instantiate-existential ("m"))
simplify
simplify
(induction trivial-integer-inductor ())
beta-reduce-repeatedly
direct-and-antecedent-inference-strategy
(cut-with-single-formula "k=0 and p=0")
simplify
(apply-macete-with-minor-premises comb-0-value-lemma)
simplify
(case-split ("p<=t"))
(backchain "with(t:zz,
forall(k,p:zz,
0<=k and k<=p and p<=t implies #(comb(p,k),zz)));")
direct-and-antecedent-inference-strategy
(case-split ("k=0"))
(backchain "with(k:zz,k=0);")
(apply-macete-with-minor-premises comb-0-value-lemma)
(case-split ("k=p"))
(backchain "with(p,k:zz,k=p);")
(apply-macete-with-minor-premises comb-m-value-lemma)
(force-substitution "p" "1+(p-1)" (0))
(apply-macete-with-minor-premises comb-ident)
sort-definedness
(backchain "with(t:zz,
forall(k,p:zz,
0<=k and k<=p and p<=t implies #(comb(p,k),zz)));")
simplify
(backchain "with(t:zz,
forall(k,p:zz,
0<=k and k<=p and p<=t implies #(comb(p,k),zz)));")
simplify
simplify
)))
```

```
(def-theorem generalized-combinatorial-identity
"forall(k,n:zz,
0<=k and 1<=n
implies
sum(0,k,lambda(j:zz,comb(n+j,j)))=comb(n+k+1,k))"
(theory h-o-real-arithmetic)
(proof
(
(induction trivial-integer-inductor ())
beta-reduce-repeatedly
(unfold-single-defined-constant (0) sum)
(apply-macete-with-minor-premises comb-0-value-lemma)
simplify
(unfold-single-defined-constant (0) sum)
simplify
(force-substitution "2+n+t" "1+(1+n+t)" (0))
(apply-macete-with-minor-premises comb-ident)
simplify
simplify
)))
```