Theorem band-011x-neg-03

• Type: A user defined theorem
• Validity: The proof is valid.
• Features:
• Comment:
• Used by: band-011x-neg-04, intshiftrzero-prop-01,
• Used by units in proved state:
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 14
• Proof steps: 25
• Used lemmas: band-011x-pos-02, band-011x-neg-02,
• Used spec theorems:
  • int-div/mod-rec
  • int-basic2/add-c
  • int-div/mod-add-01
  • int-div/mod-zero-03
  • int-div/mod-zero-05
  • int-abs/Abs-neg
• Used simplifier rules:
  • int-abs/abs-06
  • int-abs/succ-02
  • int-abs/forward-le
  • int-abs/lels-03
  • int-abs/minus-sub
  • int-abs/neg-06
  • int-abs/Abs-pos
  • int-abs/sub-le
  • int-abs/leone
  • int-abs/numls-03
  • int-abs/numsub
  • int-abs/bet
  • int-abs/sub-eq
  • int-abs/Sub-def
  • int-basic2/add-in
  • int-abs/sub-add-01
  • int-abs/sub-ls
  • int-basic2/lst-03
  • int-abs/forward-le-05
  • int-abs/neg-15
  • int-abs/sub-sub
  • int-abs/sub-add-06
  • int-abs/sub-add-09
  • int-abs/lsone
  • int-basic2/ls-01
  • int-abs/sub-ls-01
  • int-abs/succ-01
  • int-abs/mone-06
  • int-abs/numls-02
  • int-abs/neg-03
  • int-abs/negeq
  • int-div/mod-neg-01
  • int-abs/numadd-01
  • int-abs/negle-07
  • int-abs/sub-le-01
  • int-basic2/add-zero
  • int-basic2/add-a
  • int-basic2/add-c
  • int-abs/forward-lsle
  • int-abs/zero-gs
  • int-abs/zero-gels-04
  • int-abs/forward-le-04
  • int-abs/forward-lele
  • int-abs/lels-04
  • int-abs/lels-01
  • int-abs/lels
  • int-abs/neg-05
  • int-abs/forward-le-01