[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 lels-03
⊦ i < j → (¬ ¬ j ≤ i ↔ false)
Type: A user defined theorem
Validity: The proof is valid.
Features: simp, localsimp,
Comment:
Used by:
abs-09
,
abs-one-01
,
abs-sub-01
,
abs-succ
,
abssub-05
,
le-add-04
,
le-add-05
,
le-add-06
,
le-add-07
,
lels
,
lels-04
,
leone
,
les
,
mone-05
,
mone-07
,
mone-08
,
num-between
,
succ-01
,
Used by units in proved state:
int-mult
,
int-pot
,
int-gcd
,
int-div
,
intnat
,
int-square
,
int-min
,
Proof exists?: Yes
View
the proof
Infos about the proof
Proved?: Yes
Interactions: 0
Proof steps: 1
Used lemmas:
le-def
,
Used spec theorems:
Used simplifier rules: