Theorem distr

• Type: An axiom
• Validity: The proof is valid.
• Features: ls,
• Comment: used as local simprule only
• Used by: eq-dist, eq-nonzero, eq-succ, eq-succ-01, invmult-ge-neg-add, invmult-ge-pos-add, invmult-gr-neg-add, invmult-gr-pos-add, invmult-le-neg-add, invmult-le-pos-add, invmult-ls-neg-add, invmult-ls-pos-add, le-dist, le-dist-01, le-dist-02, le-neg, le-pos, ls-add-02, ls-add-03, ls-dist, ls-dist-01, ls-dist-02, ls-dist-03, ls-dist-04, ls-dist-05, ls-dist-06, ls-neg, ls-pos, minus-left, minus-one, mult-add-greater, num-distr, num-distr-add-eq1, num-distr-add-eq2, num-distr-add-le1, num-distr-add-le2, num-distr-add-ls1, num-distr-add-ls2, num-distr-addboth-eq1, num-distr-addboth-eq2, num-distr-addboth-le1, num-distr-addboth-le2, num-distr-addboth-ls1, num-distr-addboth-ls2, num-distr-eq1, num-distr-eq2, num-distr-le1, num-distr-le2, num-distr-ls1, num-distr-ls2, square-eq-01, square-eq-02, square-eq-03, square-interval, square-interval-01, square-le-04, square-le-05, square-le-05a, square-ls-02, square-ls-03, square-ls-03a, square-ls-04, square-ls-04a, square-zero-01, square-zero-01a, square-zero-02, succ-lsplit, succ-rmerge, succ-rsplit, two-le, two-le-01, two-le-02, two-le-03, two-le-04, two-ls, two-ls-01, two-ls-02, two-ls-03, two-ls-04, two-sub-03, two-sub-04, two-sub-05, zero-ge-add-02,
• Used by units in proved state:
• Proof exists?: No