```
(def-theorem cardinality-of-intervals-lemma
"forall(m:zz, n:nn, omega(n) equinumerous zz%interval(m,m+n-1))"
lemma
(theory h-o-real-arithmetic)
(proof
(
direct-inference
unfold-defined-constants
(instantiate-existential ("lambda(k:nn,if(k<n,m+k,?zz))"))
(block
(script-comment "`instantiate-existential' at (0 0 0)") extensionality
beta-reduce-repeatedly direct-inference (case-split-on-conditionals (1))
)
(block
(script-comment "`instantiate-existential' at (0 0 1)") extensionality
beta-reduce-repeatedly direct-inference (case-split-on-conditionals (0))
(block
(script-comment "`case-split-on-conditionals' at (1 0)")
(antecedent-inference "with(p:prop,forsome(x_\$7:nn,p));")
(incorporate-antecedent "with(r:rr,x_0:zz,x_0=r);") simplify
direct-and-antecedent-inference-strategy simplify
(cut-with-single-formula "0<=x_\$7") simplify
(block
(script-comment "`cut-with-single-formula' at (1)")
(cut-with-single-formula "#(x_\$7,nn)")
(incorporate-antecedent "with(x_\$7:nn,#(x_\$7,nn));")
(apply-macete-with-minor-premises nn-defining-axiom_h-o-real-arithmetic)
simplify
) )
(block
(script-comment "`case-split-on-conditionals' at (2 0)")
direct-inference (contrapose "with(p:prop,not(p));")
(block
(script-comment "`direct-inference' at (1)")
(contrapose "with(p:prop,not(forsome(x_\$7:nn,p and p)));")
(instantiate-existential ("x_0-m")) simplify simplify
) ) )
(block
(script-comment "`instantiate-existential' at (0 1)") (weaken (0))
simplify-insistently
)
(block
(script-comment "`instantiate-existential' at (1 0)") sort-definedness
direct-inference (case-split ("#(xx_0,nn)")) simplify simplify
)
)))
```