(def-theorem cut-interval-at-left 
    "forall(x,y,z:zz, x<z implies ((x<=y and y<=z) iff (y=x or (x+1<=y and y<=z))))"
    (proof
      (
        direct-and-antecedent-inference-strategy
        simplify
        simplify
        simplify
        simplify
        ))
    (theory h-o-real-arithmetic))

(def-theorem trivial-interval 
    "forall(x,y,z:zz, x=z implies ((x<=y and y<=z) iff y=x))"
    (proof
    
      (
        direct-and-antecedent-inference-strategy
        simplify
        simplify
        simplify
        ))
    (theory h-o-real-arithmetic))

(def-compound-macete
    decompose-interval
    (series
      (repeat cut-interval-at-left)
      trivial-interval
      simplify))