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