Theorem square-isSquare

• Type: A user defined theorem
• Validity: The proof is valid.
• Features: simp, localsimp,
• Comment:
• Used by:
• Used by units in proved state: decimal-complex-ops,
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 10
• Proof steps: 19
• Used lemmas: mult-def-any,
• Used spec theorems:
  • decimal/intvalue-base
  • int-div/modex
  • decimal/intvalue-rec
  • int-abs/Abs-pos
  • int-mult/dist-sub-split
• Used simplifier rules:
  • int-mult/add-mult-two
  • int-square/isSquare-square
  • int-abs/abs-01
  • int-abs/abs-07
  • int-mult/two-zero
  • int-mult/square-zero
  • int-gcd/mod-square-10
  • int-mult/one
  • int-div/div-mult-num
  • int-mult/neq-two
  • int-abs/sub-eq
  • int-mult/zero-neq-01
  • int-mult/zero-eq
  • int-div/mod-zero-num
  • int-abs/abs-zero
  • int-abs/lsone
  • int-div/nummult-ls
  • int-abs/sub-ls
  • int-basic2/add-c
  • int-basic2/add-a
  • int-abs/sub-sub
  • intnat/labs
  • int-mult/abs-eqall
  • int-abs/lels
  • int-mult/le-same-04
  • int-abs/abs-abs
  • int-mult/associativity
  • int-mult/commutativity