Theorem ls-01

• Type: A user defined theorem
• Validity: The proof is valid.
• Features: simp, localsimp,
• Comment:
• Used by: ex-ls-add, ls-02, ls-add-both, ls-succ-01, ls-succ-02, ls-zero, lst-01, lst-02, lst-03, lst-04, neq-01, nls, num-between, plst-01,
• Used by units in proved state: int-abs, int-mult, int-pot, int-div, intnat, int-square, int-basic2,
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 6
• Proof steps: 7
• Used lemmas: add-pred-01, add-succ-02, add-c, add-a, add-zero-rev,
• Used spec theorems:
  • int-basic1/ls-succ-02
• Used simplifier rules:
  • int-basic1/ls-pred-01