Theorem ls-04

• Type: A user defined theorem
• Validity: The proof is valid.
• Features: lss,
• Comment:
• Used by: addex, even-02, expand-nat, ilf-03, l, l-01, l-06, l-08, l-addone, less, less-01, less-02, less-03, less-04, less-06, lf-01, lf-02, lf-03, lf-04, lf-05, lf-06, lf-07, neq-03, nls-snd, pls, prop-ls, psh-04, psh-07, q-add-01, s-04,
• Used by units in proved state:
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 0
• Proof steps: 2
• Used lemmas: ls-03, ls-02,
• Used spec theorems:
  • Used simplifier rules: