Theorem le-pos

• Type: A user defined theorem
• Validity: The proof is valid.
• Features: localsimp, simp,
• Comment:
• Used by: le-pos-01, le-same, le-same-01, modlep, modlep-04, mult-sub-lesseq, numle-10, short-mult-max, square-ex, square-inject, square-interval, zero-ge, zero-le,
• Used by units in proved state: int-pot, int-gcd, int-div,
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 2
• Proof steps: 4
• Used lemmas: commutativity, associativity, ls-pos,
• Used spec theorems:
  • Used simplifier rules:
    • int-abs/forward-le-05
    • int-abs/lenls
    • int-abs/lels-01
    • int-abs/lels-03