Theorem div-nls-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: 2
• Proof steps: 3
• Used lemmas: neg-01, neg, div-nls, div-zero-ngr-01, abs-intro,
• Used spec theorems:
  • Used simplifier rules:
    • int-abs/forward-le-04
    • int-abs/forward-le-02
    • int-abs/Abs-pos
    • int-abs/lels
    • int-basic1/lf-02
    • int-abs/forward-lels
    • int-abs/abs-08
    • int-abs/neg-07
    • int-abs/anti
    • int-basic1/ls-01
    • int-abs/zero-gels-01
    • int-abs/negle-13
    • int-abs/zero-gels-03
    • int-abs/neg-15
    • int-basic2/add-a
    • int-basic2/add-c
    • int-abs/sub-ls
    • int-basic2/add-zero-rev
    • int-abs/neg-11
    • int-abs/neg-05
    • int-abs/lenls
    • int-abs/negle-07
    • int-abs/neg