Theorem neq-01

• Type: A user defined theorem
• Validity: The proof is valid.
• Features: simp, localsimp,
• Comment:
• Used by: eq, ls-03,
• Used by units in proved state: nat-basic2, set-union, stut-mon, nat-prime, nat-pot, nat-inf, nat-even, set-basic, nat-mult, nat, array-copy, streamseq-mon-lim, choice, inf-app-list, infinite-append,
• Proof exists?: Yes

View the proof

Infos about the proof

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