(def-recursive-constant comb_kk 
    "lambda(rec:[zz,zz,kk], a,b:kk,
            lambda(m,k:zz, if(m<0, o_kk, m=0 and k=0, i_kk, 
                              a*rec(m-1,k-1)+b*rec(m-1,k))))"
    (definition-name comb_kk)
    (theory fields))

(def-theorem comb_kk-null-lemma 
    "forall(a,b:kk, m,k:zz, m<k implies comb_kk(a,b)(m,k)=o_kk)"
    lemma
    (theory fields)
    (proof
      (
        direct-inference
        (cut-with-single-formula
          "forall(m:zz,forall(k:zz,m<k implies comb_kk(a,b)(m,k)=o_kk))")
        (backchain "with(p:prop, forall(m:zz, p))")
        direct-inference
        (case-split ("0<=m"))
        (induction trivial-integer-inductor ())
        beta-reduce-repeatedly
        direct-and-antecedent-inference-strategy
        (unfold-single-defined-constant (0) comb_kk)
        simplify
        (unfold-single-defined-constant (0 1) comb_kk)
        simplify
        (backchain "with(p:prop, forall(k:zz,p))")
        simplify
        (unfold-single-defined-constant (0) comb_kk)
        simplify
        )))

(def-theorem comb_kk-second-null-lemma 
    "forall(a,b:kk, m,k:zz, k<0 implies comb_kk(a,b)(m,k)=o_kk)"
    lemma
    (theory fields)
    (proof
      (
        direct-inference
        (cut-with-single-formula "forall(m:zz,forall(k:zz,k<0 implies comb_kk(a,b)(m,k)=o_kk))")
        (backchain "with(p:prop, forall(m:zz, p))")
        direct-inference
        (case-split ("0<=m"))
        (induction trivial-integer-inductor ())
        beta-reduce-repeatedly
        direct-and-antecedent-inference-strategy
        (unfold-single-defined-constant (0) comb_kk)
        (unfold-single-defined-constant (0 1) comb_kk)
        simplify
        (backchain-repeatedly ("with(p:prop, forall(k:zz, p))"))
        simplify
        (unfold-single-defined-constant (0) comb_kk)
        simplify
        )))

(def-theorem comb_kk-0-value-lemma 
    "forall(a,b:kk,m:zz, not(b=o_kk) and 0<=m implies comb_kk(a,b)(m,0)=b^m)"
    lemma
    (theory fields)
    (proof
      (
        (induction trivial-integer-inductor ("m"))
        beta-reduce-repeatedly
        (unfold-single-defined-constant (0) comb_kk)
        simplify
        (apply-macete-with-minor-premises comb_kk-second-null-lemma)
        simplify
        )))

(def-theorem comb_kk-m-value-lemma 
    "forall(a,b:kk,m:zz, not(a=o_kk) and 0<=m implies comb_kk(a,b)(m,m)=a^m)"
    lemma
    (theory fields)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (cut-with-single-formula
          "forall(m:zz,0<=m implies forall(k:zz,0<=k and k<=m implies comb_kk(a,b)(k,k)=a^k))")
        (backchain "with(p:prop, forall(m:zz, p))")
        auto-instantiate-existential
        simplify
        (weaken (0))
        (induction trivial-integer-inductor ())
        beta-reduce-repeatedly
        (unfold-single-defined-constant (0) comb_kk)
        simplify
        direct-and-antecedent-inference-strategy
        (cut-with-single-formula "k=0")
        simplify
        simplify
        (case-split ("k=1+t"))
        (unfold-single-defined-constant (0) comb_kk)
        simplify
        (backchain "with(b,a:kk,t:zz,
    forall(k:zz,0<=k and k<=t implies comb_kk(a,b)(k,k)=a^k));")
        (apply-macete-with-minor-premises comb_kk-null-lemma)
        simplify
        (backchain "with(b,a:kk,t:zz,
    forall(k:zz,0<=k and k<=t implies comb_kk(a,b)(k,k)=a^k));")
        simplify
        )))

(def-theorem comb_kk-ident 
    "forall(a,b:kk,k,m:zz,
          not(k=0 and m=[-1])
            implies 
          comb_kk(a,b)(1+m,k)
          ==a*comb_kk(a,b)(m,k-1)+b*comb_kk(a,b)(m,k))"
    lemma
    (theory fields)
    (proof
      (
        (unfold-single-defined-constant (0) comb_kk)
        direct-and-antecedent-inference-strategy
        (case-split ("0<=m"))
        simplify
        (case-split ("m<[-1]"))
        simplify
        (unfold-single-defined-constant (0 1) comb_kk)
        simplify
        (cut-with-single-formula "m=[-1] and not(k=0)")
        simplify
        direct-inference
        simplify
        (contrapose "with(m,k:zz,not(k=0 and m=[-1]));")
        direct-and-antecedent-inference-strategy
        )))

(def-compound-macete comb_kk-values 
    (repeat
      comb-0-value-lemma
      comb-m-value-lemma
      comb_kk-m-value-lemma
      comb_kk-0-value-lemma
      comb-ident
      comb_kk-ident))

(def-theorem comb-is-a-comb_kk 
    "forall(m,k:zz, a,b:kk,  not(a=o_kk) and not(b=o_kk) and 0<=k and k<=m implies
                    comb(m,k)*a^k*b^(m-k)
                    =comb_kk(a,b)(m,k))"
    (proof
      (
        (cut-with-single-formula
          "forall(m:zz,0<=m implies
                  forall(k,p:zz,a,b:kk,not(a=o_kk) and not(b=o_kk) and 0<=k and k<=p and p<=m 
                          implies comb(p,k)*a^k*b^(p-k)=comb_kk(a,b)(p,k)))")
        direct-and-antecedent-inference-strategy
        (backchain "with(p:prop, forall(m:zz,  0<=m implies p))")
        (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_kk-values)
        simplify
        simplify
        (case-split ("p<=t"))
        (backchain "with(r:prop, forall(k,p:zz,a,b:kk, r))")
        direct-and-antecedent-inference-strategy
        (case-split ("k=0"))
        (backchain-repeatedly ("with(k:zz,k=0);"))
        (apply-macete-with-minor-premises comb_kk-values)
        simplify
        (case-split ("k=p"))
        (backchain-repeatedly ("with(p,k:zz,k=p);"))
        (apply-macete-with-minor-premises comb_kk-values)
        simplify
        (force-substitution "p" "1+t" (0 1 2))
        (apply-macete-with-minor-premises comb_kk-values)
        (backchain-backwards "with(r:prop, forall(k,p:zz,a,b:kk, r))")
        (backchain-backwards "with(r:prop, forall(k,p:zz,a,b:kk, r))")
        direct-and-antecedent-inference-strategy
        simplify
        simplify
        simplify
        (weaken (2 4 6 7 8 12))
        (apply-macete-with-minor-premises external-multiplication-conversion)
        simplify
        simplify
        ))
    (theory fields))

(def-theorem com_kk-definedness 
    "forall(a,b:kk,m,k:zz, #(comb_kk(a,b)(m,k)))"
    (theory fields)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (case-split ("m<0"))
        (unfold-single-defined-constant (0) comb_kk)
        simplify
        (cut-with-single-formula
          "forall(m:zz, 0<=m implies forall(p,k:zz, 0<=p and p<=m implies #(comb_kk(a,b)(p,k))))")
        (backchain "with(p:prop, forall(m:zz, p))")
        (instantiate-existential ("m"))
        simplify
        simplify
        (weaken (0))
        (induction trivial-integer-inductor ())
        beta-reduce-repeatedly
        direct-and-antecedent-inference-strategy
        (cut-with-single-formula "#(comb_kk(a,b)(0,k))")
        (cut-with-single-formula "p=0")
        simplify
        simplify
        (unfold-single-defined-constant (0) comb_kk)
        (unfold-single-defined-constant (0 1) comb_kk)
        simplify
        (case-split ("p<=t"))
        (backchain "with(r:prop, forall(p:zz, r))")
        direct-and-antecedent-inference-strategy
        (force-substitution "p" "1+t" (0))
        (apply-macete-with-minor-premises comb_kk-ident)
        simplify
        direct-and-antecedent-inference-strategy
        (backchain "with(r:prop, forall(p:zz, r))")
        simplify
        (backchain "with(r:prop, forall(p:zz, r))")
        simplify
        )))
			              

(def-constant diffuse 
    "lambda(a,b:kk, lambda(rho:[zz,kk], lambda(j:zz, a*rho(j)+b*rho(j-1))))"
    (theory fields))

(def-theorem diffuse_comb 
    "forall(m:zz,a,b:kk,
          0<=m
            implies 
          diffuse(a,b)(lambda(j:zz,comb_kk(b,a)(m,j)))
          =lambda(j:zz,comb_kk(b,a)(1+m,j)))"
    (theory fields)
    (proof
      (
        (unfold-single-defined-constant (0) diffuse)
        direct-and-antecedent-inference-strategy
        extensionality
        beta-reduce-repeatedly
        direct-and-antecedent-inference-strategy
        (apply-macete-with-minor-premises comb_kk-ident)
        simplify
        )))

(def-theorem expansion-lemma 
    "forall(a,b:kk,m,n,p:zz,rho:[zz,kk],
          total_q{rho,[zz,kk]} and m-1<=n
            implies 
          sum(m,n,rho)*(a+b)
          =sum(m,n+1,diffuse(a,b)(rho))-a*rho(n+1)- b*rho(m-1))"
    (theory fields)
    (proof
      (
        (unfold-single-defined-constant (0) diffuse)
        (apply-macete tr%monoid-prod-out)
        (induction trivial-integer-inductor ())
        beta-reduce-repeatedly
        (apply-macete-with-minor-premises tr%monoid-null-prod)
        simplify
        )))

(def-theorem binomial-expansion-lemma 
    "forall(a,b:kk,m,n,p:zz, 1<=n and 0<=m
            implies 
          sum(0,m,lambda(j:zz,comb_kk(b,a)(m,j)))*(a+b)^n=
          sum(0,m+n,lambda(j:zz,comb_kk(b,a)(m+n,j))))"
    (theory fields)
    lemma
    (proof
      (
        (induction trivial-integer-inductor ("n"))
        (block 
            (script-comment "`induction' at (0 0 0 0 0 0 0)") beta-reduce-repeatedly
            (force-substitution "(a+b)^1" "a+b" (0))
            (block 
	(script-comment "`force-substitution' at (0)")
	(apply-macete-with-minor-premises expansion-lemma)
	(block 
	    (script-comment "`apply-macete-with-minor-premises' at (0)")
	    beta-reduce-repeatedly (apply-macete comb_kk-null-lemma)
	    (apply-macete comb_kk-second-null-lemma)
	    (apply-macete-with-minor-premises diffuse_comb) simplify
	    (apply-macete-with-minor-premises sum_kk-definedness)
	    direct-and-antecedent-inference-strategy beta-reduce-repeatedly
	    (apply-macete-with-minor-premises com_kk-definedness)
	    )
	(block 
	    (script-comment "`apply-macete-with-minor-premises' at (1)")
	    insistent-direct-inference beta-reduce-repeatedly
	    (apply-macete-with-minor-premises com_kk-definedness)
	    ) )
            simplify
            )
        (block 
            (script-comment "`induction' at (0 0 0 0 0 0 1 0 0 0 0)")
            (force-substitution "sum(0,m,lambda(j:zz,comb_kk(b,a)(m,j)))*(b+a)^(1+t)"
			    "sum(0,m,lambda(j:zz,comb_kk(b,a)(m,j)))*(b+a)^t*(a+b)" (0)
			    )
            (block 
	(script-comment "`force-substitution' at (0)")
	(backchain "with(k:kk,k=k);")
	(apply-macete-with-minor-premises expansion-lemma)
	(block 
	    (script-comment "`apply-macete-with-minor-premises' at (0)")
	    beta-reduce-repeatedly (apply-macete comb_kk-null-lemma)
	    (apply-macete comb_kk-second-null-lemma)
	    (apply-macete-with-minor-premises diffuse_comb) simplify
	    (apply-macete-with-minor-premises sum_kk-definedness)
	    beta-reduce-repeatedly
	    (apply-macete-with-minor-premises com_kk-definedness)
	    )
	(block 
	    (script-comment "`apply-macete-with-minor-premises' at (1)")
	    insistent-direct-inference beta-reduce-repeatedly
	    (apply-macete-with-minor-premises com_kk-definedness)
	    ) )
            simplify
            )
        )))
(make-tex-correspondence "kk" "\{ \\bf k \}")

(def-theorem binomial-theorem 
    "forall(a,b:kk, n:zz, 1<=n and not(a=o_kk) and not(b=o_kk) implies
                        (a+b)^n=sum(0,n,lambda(j:zz,comb(n,j)*b^j*a^(n-j))))"
    (theory fields)
    (usages transportable-macete)
    (proof
      (
        (force-substitution "(a+b)^n" "sum(0,0,lambda(j:zz,comb_kk(b,a)(0,j)))*(a+b)^n" (0))
        (apply-macete-with-minor-premises binomial-expansion-lemma)
        (apply-macete-with-minor-premises tr%local-context-introduction-for-monoid-prod)
        beta-reduce-repeatedly
        (apply-macete-with-minor-premises comb-is-a-comb_kk)
        simplify
        (apply-macete-with-minor-premises sum_kk-definedness)
        beta-reduce-repeatedly
        direct-and-antecedent-inference-strategy
        simplify
        (apply-macete-with-minor-premises com_kk-definedness)
        (apply-macete-with-minor-premises tr%monoid-triv-prod)
        beta-reduce-repeatedly
        (unfold-single-defined-constant (0) comb_kk)
        simplify
        )))

(def-theorem ()
    "lambda(m:zz,y:rr,y*m)
        =lambda(k:zz,m:rr,if(0<k, m*k, k=0, 0, m*k))"
    lemma
    (theory h-o-real-arithmetic)
    (proof
      (
        extensionality
        beta-reduce-repeatedly
        direct-and-antecedent-inference-strategy
        (case-split ("0<x_0"))
        simplify
        simplify
        (case-split ("x_0=0"))
        simplify
        simplify
        )))

(def-theorem ()
    "forall(h_0:[zz,rr,rr],
          forall(u_0:zz,u_1:rr,
              #(if(0<u_0,
                      u_1+h_0([-1]+u_0,u_1),
                      u_0=0,
                      0,
                      [-1]*h_0([-1]*u_0,u_1)))
                implies 
              if(0<u_0,
                  u_1+h_0([-1]+u_0,u_1),
                  u_0=0,
                  0,
                  [-1]*h_0([-1]*u_0,u_1))
              =h_0(u_0,u_1))
            implies 
          forall(u_0:zz,u_1:rr,u_1*u_0=h_0(u_0,u_1)))"
    lemma
    (theory h-o-real-arithmetic)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (cut-with-single-formula " forall(u_0:zz,u_1:rr,
                    if(0<u_0, u_1+h_0([-1]+u_0,u_1), u_0=0, 0, [-1]*h_0([-1]*u_0,u_1)) =h_0(u_0,u_1))")
        (weaken (1))
        (case-split ("1<=u_0"))
        (induction trivial-integer-inductor ("u_0"))
        beta-reduce-repeatedly
        (backchain-backwards "with(p:prop,  forall(u_0:zz,u_1:rr, p))")
        simplify
        (backchain-backwards "with(p:prop,  forall(u_0:zz,u_1:rr, p))")
        simplify
        (instantiate-universal-antecedent "with(p:prop,  forall(u_0:zz,u_1:rr, p))" ("1+t" "u_1"))
        (incorporate-antecedent "with(a,b,c,d:rr,p,q:prop, if(p,a,q,b,c)=d)")
        simplify
        (case-split ("u_0=0"))
        (backchain-backwards "with(p:prop,  forall(u_0:zz,u_1:rr, p))")
        simplify
        (backchain-backwards "with(p:prop,  forall(u_0:zz,u_1:rr, p))")
        simplify
        (cut-with-single-formula "forall(u_0:zz,u_1:rr, 1<=u_0 implies u_1*u_0=h_0(u_0,u_1))")
        (backchain-backwards "with(h_0:[zz,rr,rr],
    forall(u_0:zz,u_1:rr,1<=u_0 implies u_1*u_0=h_0(u_0,u_1)));")
        simplify
        (weaken (0 1))
        direct-and-antecedent-inference-strategy
        direct-and-antecedent-inference-strategy
        (backchain "with(p:prop,  forall(u_0:zz,u_1:rr, p))")
        (cut-with-single-formula "forall(u_0:zz,u_1:rr, #(h_0(u_0,u_1)))")
        (case-split ("0<u_0"))
        simplify
        (case-split ("u_0=0"))
        simplify
        simplify
        insistent-direct-inference
        (case-split ("1<=u_0"))
        (induction trivial-integer-inductor ("u_0"))
        beta-reduce-repeatedly
        (backchain-backwards "with(p:prop,  forall(u_0:zz,u_1:rr, p))")
        simplify
        (backchain-backwards "with(p:prop,  forall(u_0:zz,u_1:rr, p))")
        simplify
        (backchain-backwards "with(p:prop,  forall(u_0:zz,u_1:rr, p))")
        simplify
        (case-split ("u_0=0"))
        (backchain-backwards "with(p:prop,  forall(u_0:zz,u_1:rr, p))")
        simplify
        (backchain-backwards "with(p:prop,  forall(u_0:zz,u_1:rr, p))")
        simplify
        (cut-with-single-formula "forall(u_0:zz,u_1:rr, 1<=u_0 implies #(h_0(u_0,u_1)))")
        (backchain "with(h_0:[zz,rr,rr],
    forall(u_0:zz,u_1:rr,1<=u_0 implies #(h_0(u_0,u_1))));")
        simplify
        (weaken (0 1))
        direct-and-antecedent-inference-strategy
        )))

(def-theorem ()
    "^
      =lambda(x:rr,n:zz,
      if(not(x=0),
          iota(f_0:[zz,rr,rr],
              forall(x_0:zz,x_1:rr,
                  if_form(not(x_1=0),
                      #(f_0(x_0,x_1)) implies not(f_0(x_0,x_1)=0),
                      not(#(f_0(x_0,x_1)))))
                and 
              f_0
              =lambda(k:zz,m:rr,
                    if(not(m=0),
                        if(0<k,
                            lambda(x,y:rr,if(x=0 or y=0, ?rr, x*y))
                              (m,f_0([-1]+k,m)),
                            k=0,
                            1,
                            lambda(x:rr,if(x=0, ?rr, 1/x))(f_0([-1]*k,m))),
                        ?rr))
                and 
              forall(h_0:[zz,rr,rr],
                  forall(x_0:zz,x_1:rr,
                      if_form(not(x_1=0),
                          #(h_0(x_0,x_1)) implies not(h_0(x_0,x_1)=0),
                          not(#(h_0(x_0,x_1)))))
                    and 
                  h_0
                  =lambda(k:zz,m:rr,
                        if(not(m=0),
                            if(0<k,
                                lambda(x,y:rr,if(x=0 or y=0, ?rr, x*y))
                                  (m,h_0([-1]+k,m)),
                                k=0,
                                1,
                                lambda(x:rr,if(x=0, ?rr, 1/x))
                                  (h_0([-1]*k,m))),
                            ?rr))
                    implies 
                  forall(u_0:zz,u_1:rr,
                      #(f_0(u_0,u_1)) implies 
                      f_0(u_0,u_1)=h_0(u_0,u_1))))
            (n,x),
          0<n,
          0,
          ?rr))"
    lemma
    (theory h-o-real-arithmetic)
    (proof
      (
        (instantiate-transported-theorem uniqueness-of-exponentiation-corollary
				          fields-to-rr
				          ("^"))
        (simplify-antecedent "with(r,x:rr,not(x^r=r*x));")
        (simplify-antecedent "with(r:rr,not(r=1));")
        (simplify-antecedent "with(r:rr,not(r=1));")
        (simplify-antecedent "with(p:prop,not(p));")
        (simplify-antecedent "with(r:rr,#(r));")
        (block 
          (script-comment "`instantiate-transported-theorem' at (0 1)")
          (incorporate-antecedent "with(p:prop,p);")
          simplify)
        )))

(def-theorem ()
    "lambda(m:zz,y:rr,m*y)=lambda(k:zz,m:rr,if(0<k, k*m, k=0, 0, k*m))"
    (theory h-o-real-arithmetic)
    lemma
    (proof
      (
        extensionality
        simplify
        direct-and-antecedent-inference-strategy
        (case-split ("0<x_0"))
        simplify
        (block 
            (script-comment "`case-split' at (2)") simplify (case-split ("x_0=0"))
            simplify simplify
            )
        )))

(def-translation fields-to-rr-extended 
      force-under-quick-load
      (source fields)
      (target h-o-real-arithmetic)
      (core-translation fields-to-rr)
      (constant-pairs
        (*_ext "lambda(m:zz,y:rr, m*y)")
        (^_kk ^))
      (theory-interpretation-check using-simplification))