Theorem sub-ls-01

• Type: A user defined theorem
• Validity: The proof is valid.
• Features: simp, localsimp,
• Comment:
• Used by: abs-06, abs-add-le-zero, abs-ls, abs-ls-03, abs-one-01, absls-02, absls-03, absls-04, absls-06, neg, neg-01, neg-07, neg-09, negadd, numls-01, numls-03, one-03, sub-le, zero-not,
• Used by units in proved state: int-mult, int-pot, int-gcd, int-div, intnat, int-square,
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 0
• Proof steps: 1
• Used lemmas: elim-sub,
• Used spec theorems:
  • Used simplifier rules:
    • int-basic2/ls-add-both
    • int-basic2/add-a
    • int-basic2/add-c
    • int-basic2/ls-01