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