(def-theorem ()
    "forall(s:[zz,prop],
        forall(t:zz,0<t implies s(t))
          iff 
        (s(1) and forall(t:zz,0<t implies (s(t) implies s(1+t)))))"
    (theory h-o-real-arithmetic)
    (proof
      (
        direct-inference
        direct-inference
        direct-and-antecedent-inference-strategy
        (backchain "with(s:[zz,prop],forall(t:zz,0<t implies s(t)));")
        simplify
        (backchain "with(s:[zz,prop],forall(t:zz,0<t implies s(t)));")
        simplify
        (cut-with-single-formula "forall(t:zz,1<=t implies s(t))")
        direct-and-antecedent-inference-strategy
        (backchain "with(s:[zz,prop],forall(t:zz,1<=t implies s(t)));")
        simplify
        (induction integer-inductor ("t"))
        )))

(def-theorem ()
    "forall(x:rr,#(x,qq) iff forsome(a,b:zz,x=b^[-1]*a))"
    (theory h-o-real-arithmetic)
    (proof
      (
        
        direct-and-antecedent-inference-strategy
        (instantiate-theorem zz-quotient-field ("x"))
        (instantiate-existential ("a" "b"))
        (incorporate-antecedent "with(b,a:zz,x:rr,x=a/b);")
        simplify
        (backchain "with(a,b:zz,x:rr,x=b^[-1]*a);")
        sort-definedness
        (contrapose "with(a,b:zz,x:rr,x=b^[-1]*a);")
        simplify
        )))

(def-theorem ()
    "forall(x:rr,#(x,qq) iff forsome(a,b:zz,x=a*b^[-1]))"
    (theory h-o-real-arithmetic)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (block 
            (script-comment "`direct-and-antecedent-inference-strategy' at (0 0)")
            (instantiate-theorem zz-quotient-field ("x")) (instantiate-existential ("a" "b"))
            (incorporate-antecedent "with(r,x:rr,x=r);") simplify
            )
        (block 
            (script-comment "`direct-and-antecedent-inference-strategy' at (0 1 0)")
            (backchain "with(p:prop,p);") sort-definedness (contrapose "with(p:prop,p);") simplify
            )    
        )))

(def-theorem ()
    "sub=lambda(x,y:rr,x+[-1]*y)"
    (theory h-o-real-arithmetic)
    (proof
      (
        
        extensionality
        simplify
        )))

(def-theorem ()
    "<= = lambda(x,y:rr,x=y or x<y)"
    (theory h-o-real-arithmetic)
    (proof
      (
        extensionality
        simplify
        direct-and-antecedent-inference-strategy
        simplify
        simplify
        simplify
        )))
        

(def-theorem ()
    "^
      =lambda(r:rr,n:zz,
            if(n<0, 1/r^(-n), 2<=n, r^n, 1=n, r, not(r=0), 1, ?rr))"
    (theory h-o-real-arithmetic)
    (proof
      (
        extensionality
        beta-reduce-repeatedly
        direct-and-antecedent-inference-strategy
        (case-split ("x_1<0"))
        (block 
            (script-comment "node added by `case-split' at (1)")
            simplify
            (case-split ("x_0=0"))
            simplify
            simplify)
        (block 
            (script-comment "node added by `case-split' at (2)")
            (case-split ("1=x_1"))
            simplify
            (block 
	(script-comment "node added by `case-split' at (2)")
	(case-split ("2<=x_1"))
	simplify
	(block 
	    (script-comment "node added by `case-split' at (2)")
	    (cut-with-single-formula "x_1=0")
	    (block 
	        (script-comment "node added by `cut-with-single-formula' at (0)")
	        simplify
	        (case-split ("x_0=0"))
	        simplify
	        simplify)
	    simplify)))
        )))

(def-theorem ()
    "forall(h_0:[rr,zz,rr],
        forall(u_0:rr,u_1:zz,
            #(if(u_1<0,
                    h_0(u_0,[-1]*u_1)^[-1],
                    2<=u_1,
                    h_0(u_0,[-1]+u_1)*u_0,
                    1=u_1,
                    u_0,
                    not(u_0=0),
                    1,
                    ?rr))
              implies 
            if(u_1<0,
                h_0(u_0,[-1]*u_1)^[-1],
                2<=u_1,
                h_0(u_0,[-1]+u_1)*u_0,
                1=u_1,
                u_0,
                not(u_0=0),
                1,
                ?rr)
            =h_0(u_0,u_1))
          implies 
        forall(u_0:rr,u_1:zz,
            #(u_0^u_1) implies u_0^u_1=h_0(u_0,u_1)))"
    (theory h-o-real-arithmetic)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (cut-with-single-formula "2<=u_1 or 1=u_1 or 0=u_1 or u_1<0")
        (antecedent-inference "with(u_1:zz,2<=u_1 or 1=u_1 or 0=u_1 or u_1<0);")
        (induction trivial-integer-inductor ("u_1"))
        beta-reduce-repeatedly
        direct-and-antecedent-inference-strategy
        (backchain-backwards "with(p,q:prop,forall(u_0:rr,u_1:zz,p implies q))")
        simplify
        (cut-with-single-formula "u_0^2=h_0(u_0,1)*u_0")
        direct-inference
        (backchain-backwards "with(p,q:prop,forall(u_0:rr,u_1:zz,p implies q))")
        simplify
        (backchain-backwards "with(p,q:prop,forall(u_0:rr,u_1:zz,p implies q))")
        simplify
        (backchain-backwards "with(h_0:[rr,zz,rr],t:zz,u_0:rr,u_0^t=h_0(u_0,t));")
        simplify
        (backchain-backwards "with(p,q:prop,forall(u_0:rr,u_1:zz,p implies q))")
        simplify
        (backchain-backwards "with(p,q:prop,forall(u_0:rr,u_1:zz,p implies q))")
        simplify
        (contrapose "with(u_1:zz,u_0:rr,#(u_0^u_1));")
        simplify
        (cut-with-single-formula "forall(u_1:zz,1<=u_1 implies u_0^u_1=h_0(u_0,u_1))")
        (force-substitution "u_0^u_1" "(u_0^(-u_1))^[-1]" (0))
        (backchain "with(h_0:[rr,zz,rr],u_0:rr,
    forall(u_1:zz,1<=u_1 implies u_0^u_1=h_0(u_0,u_1)));")
        simplify
        (force-substitution "h_0(u_0,[-1]*u_1)^[-1]=h_0(u_0,u_1)"
			"h_0(u_0,u_1)=h_0(u_0,[-1]*u_1)^[-1]" (0))
        (backchain-backwards "with(p,q:prop,forall(u_0:rr,u_1:zz,p implies q))")
        (cut-with-single-formula "not(u_0=0)")
        simplify
        (backchain-backwards "with(h_0:[rr,zz,rr],u_0:rr,
    forall(u_1:zz,1<=u_1 implies u_0^u_1=h_0(u_0,u_1)));")
        simplify
        (contrapose "with(u_1:zz,u_0:rr,#(u_0^u_1));")
        simplify
        simplify
        (cut-with-single-formula "not(u_0=0)")
        simplify
        (weaken (0 1))
        direct-and-antecedent-inference-strategy
        (cut-with-single-formula "1=u_1 or 2<=u_1")
        (antecedent-inference "with(u_1:zz,1=u_1 or 2<=u_1);")
        (weaken (1))
        (cut-with-single-formula "#(u_0^u_1)")
        simplify
        (weaken (1))
        (cut-with-single-formula "#(u_0^u_1)")
        simplify
        simplify
        simplify
        )))


(def-translation complete-ordered-field-interpretable 
    (source complete-ordered-field)
    (target  h-o-real-arithmetic)
    (constant-pairs 
      (^ ^)
      (sub sub)
      (<= <=))
    (theory-interpretation-check using-simplification))