Theorem modlep-03

• Type: A user defined theorem
• Validity: The proof is valid.
• Features:
• Comment:
• Used by: modeqp-copied, modlep-04, modneqp,
• Used by units in proved state: int-pot, int-div,
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 3
• Proof steps: 9
• Used lemmas: commutativity, associativity, one, ls-add-03, modlep-02,
• Used spec theorems:
  • int-abs/Abs-pos
• Used simplifier rules:
  • int-basic2/add-zero-rev
  • int-abs/sub-eq
  • int-abs/forward-le-05
  • int-abs/elim-sub
  • int-basic2/eq
  • int-abs/succ-01
  • int-abs/sub-le
  • int-abs/sub-add-01
  • int-abs/lels
  • int-basic1/irref
  • int-abs/lels-01
  • int-abs/abs-06
  • int-basic2/add-less
  • int-abs/forward-le-01
  • int-abs/forward-le
  • int-abs/lep-02
  • int-basic1/lst-01
  • int-basic2/ls-01
  • int-basic2/add-a
  • int-basic2/add-c
  • int-basic2/ls
  • int-abs/lep
  • int-abs/lels-02
  • int-abs/abs-08
  • int-abs/neg-13
  • int-basic2/zero-02
  • int-abs/abs-16
  • int-abs/numls-03
  • int-basic1/ls-01
  • int-abs/neg-07
  • int-basic2/zero-01
  • int-abs/negle-07
  • int-basic1/lf-01
  • int-basic1/trans
  • int-abs/forward-lsle
  • int-abs/forward-le-02
  • int-abs/forward-lels
  • int-abs/forward-le-04
  • int-abs/forward-lele
  • int-basic1/numlsf
  • int-basic2/succ-01
  • int-basic2/lst-04
  • int-abs/absls-01