Theorem gcd-rec-sub-01

• Type: A user defined theorem
• Validity: The proof is valid.
• Features:
• Comment:
• Used by: gcd-divides-both-h,
• Used by units in proved state:
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 44
• Proof steps: 54
• Used lemmas: gcd-rec-sub-02, gcd-same-01, gcd-neg, gcd-abs-rew-02, gcd-zero-03, gcd-same, gcd-com, gcd-zero-04, gcd-rec-sub,
• Used spec theorems:
  • int-abs/Abs-neg
  • int-abs/lels
  • int-basic1/l
• Used simplifier rules:
  • int-abs/elim-sub
  • int-abs/sub-add
  • int-abs/forward-le-04
  • int-abs/negle-13
  • int-basic2/add-zero
  • int-abs/zero-gels-01
  • int-abs/neg-06
  • int-abs/neg-15
  • int-abs/sub-add-09
  • int-abs/Abs-pos
  • int-mult/add-mult-two
  • int-basic2/zero-01
  • int-abs/forward-le-05
  • int-basic1/lst-01
  • int-basic2/add-in
  • int-abs/sub-sub-03
  • int-abs/abseq
  • int-abs/forward-le-02
  • int-basic2/add-a
  • int-abs/lels-02
  • int-abs/lep-01
  • int-abs/subsub
  • int-abs/neg-07
  • int-abs/lels
  • int-abs/lels-03
  • int-abs/abs-07
  • int-abs/negeq
  • int-abs/abs-neg
  • int-abs/neg-12
  • int-basic2/add-c
  • int-abs/abs-18
  • int-abs/lels-01
  • int-basic1/ls-01
  • int-abs/abs-16
  • int-abs/abs-08
  • int-abs/subneg
  • int-abs/neg-13
  • int-abs/neg