Theorem short-larger

• Type: A user defined theorem
• Validity: The proof is valid.
• Features:
• Comment:
• Used by:
• Used by units in proved state:
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 4
• Proof steps: 15
• Used lemmas: sis-sub-2pot, sis-pos-low, sis-pos-high, short-inj,
• Used spec theorems:
  • Used simplifier rules:
    • int-basic1/irref
    • int-abs/Sub-def
    • int-basic2/eq
    • int-abs/lels-03
    • int-basic1/numlslsdel-01
    • int-basic1/forward-pos
    • int-abs/forward-le-05
    • int-abs/forward-lels
    • int-abs/sub-eq
    • int-abs/numle-02
    • int-basic2/add-a
    • int-basic2/add-c
    • int-abs/numls-02
    • int-abs/numlsledel-01
    • int-abs/numleledel-01
    • int-div/mod-add
    • int-abs/elim-sub
    • int-div/mod-zero-07
    • int-abs/sub-le-01
    • int-abs/lels
    • int-basic1/ls-01
    • int-abs/lels-01
    • int-abs/forward-le
    • int-abs/forward-le-01