Theorem ceil-triang

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

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 8
• Proof steps: 9
• Used lemmas: ceil-notls, ceil-ls-add-one,
• Used spec theorems:
  • real-abs/forward-lsle
  • real-abs/ple
  • real-abs/sub-def
  • real-basic/eqint-sub
  • real-basic/eqint-add
• Used simplifier rules:
  • real-abs/sub-def
  • real-basic/negladd-ls
  • real-abs/lels
  • real-abs/lels-03
  • real-basic/add-assoc
  • real-basic/add-comm
  • int-abs/le-def
  • real-abs/le-def
  • real-basic/ls-num
  • int-abs/sub-ls
  • int-abs/succ-02
  • int-basic2/add-a
  • int-basic2/add-c
  • int-abs/lenls