Documentation
Batteries
.
Data
.
Range
.
Lemmas
Search
return to top
source
Imports
Init
Batteries.Tactic.Alias
Batteries.Tactic.SeqFocus
Imported by
Std
.
Range
.
size_stop_le_start
Std
.
Range
.
size_step_1
source
theorem
Std
.
Range
.
size_stop_le_start
(
r
:
Range
)
:
r
.
stop
≤
r
.
start
→
r
.
size
=
0
source
theorem
Std
.
Range
.
size_step_1
(
start
stop
:
Nat
)
:
[
start
:
stop
]
.
size
=
stop
-
start