Theorem nummult-ls-03

• Type: A user defined theorem
• Validity: The proof is valid.
• Features: simp, localsimp,
• Comment:
• Used by: nummult-ls-03-01,
• Used by units in proved state:
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 8
• Proof steps: 17
• Used lemmas: div-elim2,
• Used spec theorems:
  • int-abs/add-rew
  • int-abs/add-shift
  • int-abs/lels
  • int-mult/modlep-02
  • int-mult/modlsp-01
• Used simplifier rules:
  • int-abs/elim-sub
  • int-basic2/add-zero
  • int-abs/sub-ls-01
  • int-abs/lels
  • int-abs/leone
  • int-abs/forward-le-05
  • int-abs/forward-le-02
  • int-mult/succ-rmerge
  • int-abs/sub-eq
  • int-abs/zero-gels-01
  • int-mult/ls-dist-03
  • int-abs/forward-le-04
  • int-abs/forward-lels
  • int-abs/ler
  • int-mult/ls-pos
  • int-abs/le-add
  • int-abs/sub-le-01
  • int-abs/lsone
  • int-abs/succ-02
  • int-abs/sub-ls
  • int-basic2/add-in
  • int-abs/Sub-def
  • int-abs/succ-01
  • int-abs/lels-01
  • int-abs/les
  • int-basic2/add-a
  • int-basic2/add-c
  • int-abs/forward-lsle
  • int-mult/zero-ls
  • int-abs/numls-03
  • int-mult/associativity
  • int-mult/commutativity
  • int-basic2/ls-02
  • int-mult/ls-dist
  • int-abs/lenls