(def-constant discrete%set 
    "lambda(s:sets[rr], forsome(a:rr,0<a and forall(x,y:rr, x<y implies a<=y-x)))"
    (theory h-o-real-arithmetic))

(def-theorem discrete-sets-contain-sup-lemma 
    "forall(s:sets[rr], discrete%set(s) and #(sup(s)) implies
                    forsome(a:rr,0<a and forall(x:rr, x in s implies x=sup(s) or x<=sup(s)-a)))"
    (theory h-o-real-arithmetic)
    (proof
      (
        (unfold-single-defined-constant (0) discrete%set)
        direct-and-antecedent-inference-strategy
        auto-instantiate-existential
        (cut-with-single-formula "forsome(z:rr, z in s and x<z and sup(s)-a<=z and z<=sup(s))")
        (antecedent-inference "with(a,x:rr,s:sets[rr],
    forsome(z:rr,
        z in s and x<z and sup(s)-a<=z and z<=sup(s)));")
        (instantiate-universal-antecedent "with(a:rr,forall(x,y:rr,x<y implies a<=y-x));" ("x" "z"))
        simplify
        (cut-with-single-formula "forall(z:rr, z<sup(s) implies forsome(x:rr, x in s and z<x))")
        (instantiate-universal-antecedent "with(s:sets[rr],
    forall(z:rr,
        z<sup(s) implies forsome(x:rr,x in s and z<x)));" ("max(x,sup(s)-a)"))
        (contrapose "with(a:rr,s:sets[rr],x:rr,not(max(x,sup(s)-a)<sup(s)));")
        (weaken (0))
        (cut-with-single-formula "x<=sup(s)")
        (unfold-single-defined-constant (0) max)
        (case-split-on-conditionals (0))
        (apply-macete-with-minor-premises tr%minorizes-property-of-prec%sup)
        direct-inference
        (instantiate-existential ("x"))
        simplify
        (instantiate-existential ("x_$0"))
        (cut-with-single-formula "x<=max(x,sup(s)-a)")
        simplify
        (apply-macete-with-minor-premises maximum-1st-arg)
        (cut-with-single-formula "sup(s)-a<=max(x,sup(s)-a)")
        simplify
        (apply-macete-with-minor-premises maximum-2nd-arg)
        (apply-macete-with-minor-premises tr%minorizes-property-of-prec%sup)
        direct-inference
        (instantiate-existential ("x_$0"))
        simplify
        direct-and-antecedent-inference-strategy
        (force-substitution "z" "sup(s)-(sup(s)-z)" (0))
        (apply-macete-with-minor-premises sup-minus-epsilon-corollary)
        simplify
        simplify
        )))

(def-theorem empty-indic-sup-is-undefined 
    "not(#(sup(empty_indic{rr})))"
    (theory h-o-real-arithmetic)
    (proof
      (
        
        (cut-with-single-formula " #(sup(empty_indic{rr})) implies sup(empty_indic{rr})<=sup(empty_indic{rr})-1")
        (antecedent-inference "with(p,q:prop, p implies q)")
        (simplify-antecedent "sup(empty_indic{rr})<=sup(empty_indic{rr})-1;")
        direct-and-antecedent-inference-strategy
        (apply-macete-with-minor-premises tr%lub-property-of-prec%sup)
        direct-and-antecedent-inference-strategy
        (unfold-single-defined-constant (0) majorizes)
        direct-and-antecedent-inference-strategy
        (contrapose "with(x_$0:rr,x_$0 in empty_indic{rr});")
        simplify-insistently
        )))

(def-theorem discrete-sets-contain-sup 
    "forall(s:sets[rr], discrete%set(s) and #(sup(s)) implies sup(s) in s)"
    (theory h-o-real-arithmetic)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (cut-with-single-formula "forsome(a:rr,0<a and forall(x:rr, x in s implies x=sup(s) or x<=sup(s)-a))")
        (antecedent-inference "with(s:sets[rr],
    forsome(a:rr,
        0<a
          and 
        forall(x:rr,x in s implies x=sup(s) or x<=sup(s)-a)));")
        (antecedent-inference "with(s:sets[rr],a:rr,
    0<a
      and 
    forall(x:rr,x in s implies x=sup(s) or x<=sup(s)-a));")
        (contrapose "with(s:sets[rr],discrete%set(s));")
        (cut-with-single-formula "sup(s)<=sup(s)-a")
        (contrapose "with(a:rr,s:sets[rr],sup(s)<=sup(s)-a);")
        simplify
        (apply-macete-with-minor-premises tr%lub-property-of-prec%sup)
        direct-inference
        (unfold-single-defined-constant (0) majorizes)
        direct-and-antecedent-inference-strategy
        (backchain "with(a:rr,s:sets[rr],
    forall(x:rr,x in s implies x=sup(s) or x<=sup(s)-a));")
        direct-and-antecedent-inference-strategy
        (contrapose "with(s:sets[rr],not(sup(s) in s));")
        (backchain-backwards "with(s:sets[rr],x_$0:rr,x_$0=sup(s));")
        (apply-macete-with-minor-premises discrete-sets-contain-sup-lemma)
        direct-and-antecedent-inference-strategy
        )))

(def-constant preceding 
    "lambda(s:sets[rr],a:rr, sup(indic{x:rr,x in s and x<a}))"
    (theory h-o-real-arithmetic))

(def-theorem preceding-for-discrete-sets 
    "forall(s:sets[rr], x:rr, discrete%set(s) and #(preceding(s,x)) implies preceding(s,x) in s)"
    (proof
      (
        (unfold-single-defined-constant (0 1) preceding)
        direct-and-antecedent-inference-strategy
        (cut-with-single-formula "forall(a,b:sets[rr],sup(a) in a and a subseteq b implies sup(a) in b)")
        (backchain "forall(a,b:sets[rr],sup(a) in a and a subseteq b implies sup(a) in b)")
        direct-and-antecedent-inference-strategy
        (apply-macete-with-minor-premises discrete-sets-contain-sup)
        direct-and-antecedent-inference-strategy
        (incorporate-antecedent "with(s:sets[rr],discrete%set(s));")
        unfold-defined-constants
        simplify-insistently
        simplify
        ))
    (theory h-o-real-arithmetic))

(def-theorem preceding-defined 
    "forall(s:sets[rr], x:rr,  #(preceding(s,x)) iff forsome(y:rr, y in s and y<x))"
    (theory h-o-real-arithmetic)
    (proof
      (
        (unfold-single-defined-constant (0) preceding)
        direct-and-antecedent-inference-strategy
        (cut-with-single-formula "forall(s:sets[rr], s =empty_indic{rr} implies not(#(sup(s))))")
        (contrapose "with(t:rr, #(t))")
        (backchain "forall(s:sets[rr],s=empty_indic{rr} implies not(#(sup(s))));")
        simplify-insistently
        extensionality
        beta-reduce-repeatedly
        direct-and-antecedent-inference-strategy
        (instantiate-universal-antecedent "with(x:rr,s:sets[rr],forall(y:rr,not(y in s) or not(y<x)));" ("x_0"))
        simplify
        simplify
        direct-and-antecedent-inference-strategy
        (backchain "with(s_$0:sets[rr],s_$0=empty_indic{rr});")
        (apply-macete-with-minor-premises empty-indic-sup-is-undefined)
        (apply-macete-with-minor-premises tr%prec%sup-defined)
        direct-and-antecedent-inference-strategy
        simplify-insistently
        auto-instantiate-existential
        (instantiate-existential ("x"))
        (unfold-single-defined-constant (0) majorizes)
        simplify-insistently
        )))