Theorem ls-natinf-to-nat-2-1

• Type: A user defined theorem
• Validity: The proof is valid.
• Features: localsimp, simp,
• Comment:
• Used by: add-not-less, leq-notgradd, less-less-leftsucc, ls-natinf-to-nat-2-2, ls-natinf-to-nat-3-1,
• Used by units in proved state: stream, stut-mon, mon-lim-filter-count, streamseq-mon-lim, inf-app-list, infinite-append,
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 2
• Proof steps: 2
• Used lemmas: less-fin, add-fin,
• Used spec theorems:
  • Used simplifier rules: