(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 )))