[Imprint]
[Data Privacy Statement]
[E-Mail]
View
long theorem info
. View
the proof
. Back to
main index
. View
the specification
. View
theorem base summary
, View
theorem base listing
, the
used properties by spec
, the
dependency list
, the
symbol table
,
Theorem square-ge-one
⊦ 1.r ≤ r * r ↔ 1.r ≤ r ∨ r + 1.r ≤ 0.r
Type: A user defined theorem
Validity: The proof is valid.
Features: s, ls,
Comment:
Used by:
square-ls-04
,
Used by units in proved state:
Proof exists?: Yes
View
the proof
Infos about the proof
Proved?: Yes
Interactions: 1
Proof steps: 6
Used lemmas:
abs-ite
,
mult-com
,
mult-ass
,
mult-one
,
square-le
,
Used spec theorems:
Used simplifier rules:
real-abs
/
abs-one
real-abs
/
le-def
real-abs
/
forward-lsle
real-abs
/
negle-07
real-basic
/
add-comm
real-abs
/
lels-03
real-basic
/
irref
real-abs
/
lels
real-abs
/
forward-lele
real-abs
/
forward-lels
real-abs
/
lep-01
real-basic
/
add-assoc
real-basic
/
negl-ls
real-basic
/
trans
real-basic
/
ls-num