Theorem neq-01

• Type: A user defined theorem
• Validity: The proof is valid.
• Features: ss, lss,
• Comment:
• Used by: eq, l, l-03, q-add-01, succ-03,
• Used by units in proved state: rowcol-upd, matrixops, array-copy, stut-mon, set-basic, nat-mult, stream, nat-prime, streamseq-mon-lim, set-union, choice, nat-inf, inf-app-list, infinite-append, nat-pot, nat-even, natset,
• 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: