Theorem mod-div-zero

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

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 5
• Proof steps: 11
• Used lemmas: mod-not-less, mod-neg-01, div-elim-posneg, mod-neg, mod-les, abs-shift, div-eq-zero-01,
• Used spec theorems:
  • int-abs/Abs-neg
  • int-abs/numle-02
  • int-abs/neg-06
• Used simplifier rules:
  • int-basic1/lst-01
  • int-abs/abs-16
  • int-abs/forward-le-02
  • int-abs/neg-06
  • int-abs/neg-15
  • int-basic2/add-a
  • int-basic2/add-c
  • int-abs/sub-le-01
  • int-basic2/add-zero-rev
  • int-abs/forward-lsle
  • int-abs/forward-le-01
  • int-abs/lels
  • int-abs/Abs-pos
  • int-abs/negle-13
  • int-abs/abs-08
  • int-abs/neg-07
  • int-abs/lenls
  • int-abs/zero-gels-01
  • int-abs/zero-gels-04