Theorem make

• Type: A user defined theorem
• Validity: The proof is valid.
• Features: simp, localsimp,
• Comment:
• Used by: add-zero, denum-same-01, exrat, exrat-gcd1, int-add, negate, num-neg-03, num-same,
• Used by units in proved state:
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 23
• Proof steps: 43
• Used lemmas: num-pos, denominator-pos, numerator-zero-den, denominator-zero-den, denominator-zero, numerator-zero, numerator-neg2, numerator-neg1, numerator-pos, Equality, gen,
• Used spec theorems:
  • int-gcd/gcd-pos
• Used simplifier rules:
  • int-div/div-lezero
  • int-gcd/not-less-gcd
  • int-abs/forward-lels
  • int-abs/abs-16
  • int-gcd/div-gcd-is-neg-01
  • int-gcd/div-gcd-is-neg
  • int-gcd/div-gcd-not-neg
  • int-abs/neg-05
  • int-abs/forward-le-05
  • int-gcd/div-gcd-neg-not-zero
  • int-gcd/div-gcd-zero
  • int-abs/neg-10
  • int-abs/abs-neg
  • int-div/abs
  • int-gcd/gcd-abs
  • int-basic2/add-c
  • int-basic2/add-a
  • int-abs/neg-03
  • int-gcd/gcd-div-gcd
  • int-gcd/gcd-neg
  • int-abs/neg
  • int-gcd/div-gcd-is-neg-01-01
  • int-gcd/gcd-com
  • int-abs/negeq
  • int-div/neg-01
  • int-gcd/gcd-zero-zero
  • int-basic1/ls-01
  • int-abs/abs-08
  • int-div/one
  • int-gcd/gcd-one-01
  • int-abs/lels-02
  • int-abs/forward-le-02
  • int-abs/forward-le-04
  • int-abs/anti
  • int-abs/lels