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