(def-constant even 
    "lambda(i:zz, forsome(j:zz, i=2*j))"
    (theory h-o-real-arithmetic))

(def-constant odd 
    "lambda(i:zz, forsome(j:zz, i=2*j+1))"
    (theory h-o-real-arithmetic))

(def-theorem even-iff-suc-is-odd 
    "forall(n:zz, even(n) iff odd(n+1))"
    reverse
    (theory h-o-real-arithmetic)
    (proof
      (
        unfold-defined-constants
        direct-and-antecedent-inference-strategy
        (instantiate-existential ("j"))
        (instantiate-existential ("j"))
        simplify
        )))

(def-theorem odd-iff-suc-is-even 
    "forall(n:zz, odd(n) iff even(n+1))"
    reverse
    (theory h-o-real-arithmetic)
    (proof
      (
        unfold-defined-constants
        direct-and-antecedent-inference-strategy
        (instantiate-existential ("j+1"))
        simplify
        (instantiate-existential ("j-1"))
        simplify
        )))

(def-theorem natural-numbers-are-even-or-odd 
    "forall(n:nn, even(n) or odd(n))"
    (theory h-o-real-arithmetic)
    (proof
      (
        (cut-with-single-formula 
          "forall(n:zz, 0<=n implies forall(m:nn, m<=n implies (even(m) or odd(m))))")
        direct-inference
        (backchain "with(p:prop, p)")
        (instantiate-existential ("n"))
        (apply-macete-with-minor-premises nn-in-quasi-sort_h-o-real-arithmetic)
        simplify
        (induction integer-inductor ("n"))
        direct-and-antecedent-inference-strategy
        (contrapose "with(p:prop, forall(j:zz,p))")
        (instantiate-existential ("0"))
        simplify
        (cut-with-single-formula "m<=t or m=1+t")
        (antecedent-inference "with(p,q:prop, p or q)")
        (backchain "with(p:prop, forall(m:nn,p))")
        (cut-with-single-formula "even(t) or odd(t)")
        (force-substitution "m" "t+1" (0 1))
        (incorporate-antecedent "with(p,q:prop, p or q)")
        (apply-macete-locally even-iff-suc-is-odd (0) "even(t)")
        (apply-macete-locally odd-iff-suc-is-even (0) "odd(t)")
        direct-and-antecedent-inference-strategy
        simplify
        (instantiate-universal-antecedent "with(p:prop, forall(m:nn,p))" ("t"))
        (simplify-antecedent "with(p:prop, not(p))")
        simplify
        )))

(def-theorem even-and-odd-natural-numbers-are-disjoint 
    "forall(n:nn, odd(n) iff not even(n))"
    (theory h-o-real-arithmetic)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (incorporate-antecedent "with(p:prop, p)")
        unfold-defined-constants
        simplify
        direct-and-antecedent-inference-strategy
        (backchain "with(p:prop, p)")
        (weaken (0))
        (instantiate-theorem trichotomy ("j" "j_$0"))
        simplify
        simplify
        simplify
        (instantiate-theorem natural-numbers-are-even-or-odd ("n"))
        )))

(def-recursive-constant nn%quotient 
    "lambda(f:[rr,rr,rr],
          lambda(m,n:rr,if(n=0, ?rr, if(m<n,0,1+f(m-n,n)))))"
    (theory h-o-real-arithmetic)
    (definition-name nn%quotient))

(def-constant zz%quotient 
    "lambda(m,n:zz,
          if(m*n<0,
                nn%quotient(abs(m),abs(n))-1,
                nn%quotient(abs(m),abs(n))))"
    (theory h-o-real-arithmetic))