Theorem div-zero-02

• Type: A user defined theorem
• Validity: The proof is valid.
• Features:
• Comment:
• Used by: div-div-pred-01, div-minus-onediff, div-two-intro, div-twoodd-05, div-twoodd-07, one-pos,
• Used by units in proved state: int-pot,
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 4
• Proof steps: 7
• Used lemmas: Div-right, div-zero-01, div-zero-05, div-eq-zero-01, div-zero,
• Used spec theorems:
  • Used simplifier rules:
    • int-basic2/ls
    • int-abs/forward-lsle
    • int-abs/zero-gels-03
    • int-abs/absls-06
    • int-abs/forward-le-01
    • int-abs/forward-lels
    • int-abs/absle
    • int-abs/lels-03
    • int-abs/lels
    • int-abs/abs-06
    • int-basic2/ls-02
    • int-basic2/add-c
    • int-basic2/add-a
    • int-basic2/ls-01
    • int-basic2/succ-01
    • int-abs/forward-le-02
    • int-basic1/trans
    • int-basic1/lf-01
    • int-abs/forward-le-05
    • int-abs/neg-13
    • int-abs/abs-08
    • int-abs/lels-01
    • int-basic1/ls-01
    • int-abs/neg
    • int-abs/neg-07
    • int-abs/zero-gels-01
    • int-basic1/lf-02
    • int-abs/neg-10