Theorem even-not-ex

• Type: A user defined theorem
• Validity: The proof is valid.
• Features:
• Comment:
• Used by: even-add, even-mult, even-or-succ-even,
• Used by units in proved state: int-square,
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 4
• Proof steps: 6
• Used lemmas: nummult-ls, div-elim-negpos, div-elim-pospos,
• Used spec theorems:
  • Used simplifier rules:
    • int-basic1/two-ls
    • int-abs/forward-le-05
    • int-abs/forward-le-01
    • int-mult/zero-ge-add
    • int-basic2/add-in
    • int-abs/lels-01
    • int-abs/zero-gels-01
    • int-mult/eq-pos
    • int-mult/succ-rmerge
    • int-abs/sub-eq
    • int-abs/zero-gels-04
    • int-abs/lsone
    • int-abs/sub-ls
    • int-abs/minus-add
    • int-abs/forward-le-04
    • int-abs/forward-le-02
    • int-basic1/minus-one
    • int-abs/numls-02
    • int-abs/neg-13
    • int-abs/abs-08
    • int-abs/lels-02
    • int-mult/commutativity
    • int-mult/associativity
    • int-mult/odd-even
    • int-basic2/add-zero
    • int-abs/Sub-def
    • int-basic2/add-a
    • int-basic2/add-c