Theorem mult-a

• Type: A user defined theorem
• Validity: The proof is valid.
• Features: simp, localsimp,
• Comment:
• Used by: addle, addle-01, coef-01, coef-02, coef-03, coef-04, coef-05, coef-06, coef-07, coef-08, coef-09, coef-10, coef-11, coef-12, coef-13, coef-14, coef-15, coef-16, coef-17, coef-18, coef-19, coef-20, coef-21, coef-22, coef-23, dist, dist-merge, dist-sub, dist-sub-01, dist-sub-02, dist-sub-03, dist-sub-04, eq, eq-01, eq-same, ex-two, le, le-01, le-02, le-03, le-04, le-05, le-num, le-rew, le-same, le-succ, le2-02, le2-03, le2-04, leone, ls, ls-01, ls-02, ls-03, ls-03-num, ls-04, ls-05, ls-06, ls-07, ls-08, ls-09, ls-10, ls2-02, ls2-03, lssucc, lssucc-01, mod-ls, mod-neq, mod-neq-02, mod-neq-03, mod-neq-04, mod-neq-05, mod-nle, modeq, modeq-01, modls, modls-01, modls-03, modp, mult-c, mult-eq-succ, mult-eq-succ-01, mult-eq-succ-02, mult-ineq-le, mult-ineq-lt, mult-le, mult-le-01, mult-sub-less, neqone, nonumsimp-addls-01, nonumsimp-eqsucc, nonumsimp-lstwo, nonumsimp-mod-neq, nonumsimp-mod-neq-05, nonumsimp-succ, nonumsimp-twoeq, nonumsimp-twoeq-01, nonumsimp-twole, nonumsimp-twols, nonumsimp-twonle, numeral-01, numeral-03, numeral-04, numeral-05, numeral-06, numeral-07, numeral-08, numeral-09, numeral-10, numeral-11, numeral-12, numeral-15, numeral-16, numeral-17, numeral-18, numeral-19, numeral-20, numeral-21, numeral-23, numeral-24, numeral-25, numeral-26, numeral-27, numeral-28, numeral-29, numeral-30, numeral-32, numeral-33, numeral-35, numeral-36, one, one-01, one-02, rsucc, rsucc-01, sqle, sqle-01, sqle-02, sqls, sqp, sqr, sqr-01, sqr-02, sqr-03, sqr-05, sqr-06, sqr-07, sqr-08, sqr-09, square-eq, square-eq-01, square-eq-03, square-even, square-even-01, square-inject, square-interval, square-le, square-le-01, square-le-02, square-less, square-ls, square-ls-01, square-ls-02, square-ls-04, square-ls-05, square-one, square-two, sqzero, succ, succ-01, succ-merge, three, threeeq, threels, two-02, two-03, two-les-01, two-ls-01, two-one-01, two-succ-03, two-succ-04, two-succ-05, two-succ-06, two-zero-01, twoeq, twoeqf, twoeqf-01, twoeqf-02, twole, twole-01, twole-02, twols, twols-01, zero, zero-01, zero-02, zero-03, zero-04, zero-05, zero-06, zero-num,
• Used by units in proved state: nat-pair, nat-div, int-pot, nat-prime, nat-pot, nat-even, intnat, int-pair,
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 2
• Proof steps: 6
• Used lemmas: rdist, rsucc-02, mult-base,
• Used spec theorems:
  • Used simplifier rules:
    • nat-basic2/succ
    • nat-basic2/c
    • nat-basic2/a
    • nat-basic2/eq-01