Theorem mult-com

• Type: An axiom
• Validity: The proof is valid.
• Features: s, ls,
• Comment:
• Used by: abs-eqall, abs-eqneg, abs-le-one-multiple, abs-ls-multiple-one, abs-ls-one-multiple, abs-ls-same, abs-not-neg, add-mult-two, commutativity, eq-dist, eq-neg-01, eq-nonzero, eq-nonzero-01, eq-nonzero-02, eq-nonzero-03, eq-pos-01, eq-same, eq-same-01, eq-same-02, eq-same-03, eq-succ, eq-succ-01, est-nle, inv-eq, inv-le-neg, inv-le-pos, inv-ls-neg, inv-ls-pos, inv-mult, inv-mult-add-eq, inv-twice, invmult-eq, invmult-ge-neg, invmult-ge-neg-add, invmult-ge-pos, invmult-ge-pos-add, invmult-gr-neg, invmult-gr-neg-add, invmult-gr-pos, invmult-gr-pos-add, invmult-le-neg, invmult-le-neg-add, invmult-le-pos, invmult-le-pos-add, invmult-ls-neg, invmult-ls-neg-add, invmult-ls-pos, invmult-ls-pos-add, le-abs, le-dist, le-dist-01, le-dist-02, le-neg, le-neg-01, le-pos, le-pos-01, le-same, le-same-01, le-same-02, le-same-03, le-same-04, le-same-05, le-same-06, 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-forward, ls-neg, ls-neg-01, ls-pos, ls-pos-01, ls-pos-02, ls-same, ls-same-01, ls-same-02, ls-same-03, ls-same-04, ls-same-05, ls-two, ls-two-01, ls-two-02, ls-two-03, minus-left, minus-one, minus-one-01, mods-ls, mods-zero-07, mult-add-greater, mult-gt-both, mult-gt-one, mult-pos, mult-pos-pos, mult-zero, neq-not-zero, neq-not-zero-01, noeth-zero-ls, 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, ple-neg, ple-pos, ple-pos-better, pls-neg, pls-pos, pls-pos-01, pls-pos-02, pnle-neg, pnle-pos, pnls-neg, pnls-negpos, pnls-pos, pnls-posneg, posint-factor, pzero-gr, pzero-ls, square-abs, square-eq-01, square-eq-02, square-eq-03, square-eq-one, square-ge-one, square-gez, square-gez-01, square-gr-one, square-interval, square-interval-01, square-le, square-le-03, square-le-04, square-le-05, square-le-05a, square-le-one, square-lez, square-lez-01, square-ls-01, square-ls-02, square-ls-03, square-ls-03a, square-ls-04, square-ls-04a, square-ls-one, square-minus, square-zero, square-zero-01, square-zero-01a, square-zero-02, succ-lsplit, succ-rmerge, succ-rsplit, twice-le-zero, twice-ls-zero, two-eq, 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, two-sub-01, two-sub-02, two-sub-03, two-sub-04, two-sub-05, zero-eq, zero-ge, zero-ge-01, zero-ge-02, zero-ge-03, zero-ge-add-01, zero-ge-add-02, zero-ge-case, zero-gr, zero-gr-01, zero-gr-02, zero-gr-03, zero-gr-add-01, zero-gr-case, zero-le, zero-le-01, zero-le-02, zero-le-03, zero-le-case, zero-left, zero-ls, zero-ls-01, zero-ls-02, zero-ls-03, zero-ls-case, zero-neq, zero-neq-01,
• Used by units in proved state: real-limit,
• Proof exists?: No