Theorem div-div-pred-01

• Type: A user defined theorem
• Validity: The proof is valid.
• Features:
• Comment:
• Used by:
• Used by units in proved state:
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 16
• Proof steps: 30
• Used lemmas: nummult-ls, div-zero-02, one, div-mult-num-01, nummult-le-01, mod-zero-num, div-add1-negneg, div-elim-negpos, div-ls-zero, div-div-pred,
• Used spec theorems:
  • int-abs/numadd-01
  • int-mult/dist-lsplit
  • int-abs/zero-ge-01
  • int-basic1/two-ls
• Used simplifier rules:
  • int-abs/numle-03
  • int-abs/sub-eq
  • int-abs/elim-sub
  • int-basic1/numlslsdel
  • int-abs/numls-03
  • int-abs/numsub
  • int-abs/num-between
  • int-basic1/minus-one
  • int-basic2/ls
  • int-mult/zero-left
  • int-mult/numls-06
  • int-mult/one
  • int-mult/numls-04
  • int-abs/forward-lele
  • int-abs/forward-le-01
  • int-abs/Abs-pos
  • int-abs/numlsledel
  • int-abs/anti
  • int-basic1/lf-01
  • int-abs/forward-lsle
  • int-mult/ls-same-03
  • int-abs/mone-05
  • int-basic2/eq
  • int-abs/lels
  • int-abs/abs-06
  • int-abs/lels-02
  • int-abs/abs-08
  • int-abs/negeq
  • int-abs/numadd-01
  • int-basic2/add-a
  • int-basic2/add-c
  • int-abs/forward-le-02
  • int-abs/minus-add
  • int-abs/sub-add-01
  • int-abs/sub-ls
  • int-abs/lsone
  • int-abs/zero-gels-04
  • int-mult/associativity
  • int-mult/commutativity
  • int-abs/sub-le
  • int-abs/forward-le-03
  • int-abs/forward-le-04
  • int-basic1/numlsf
  • int-abs/zero-gels-03
  • int-abs/neg-13
  • int-abs/numls-02
  • int-abs/lenls
  • int-basic1/lf-02
  • int-basic2/add-zero-rev
  • int-abs/zero-gels-01
  • int-mult/zero-ls
  • int-abs/lels-03