Documentation
Init
.
Data
.
UInt
.
Lemmas
Search
Google site search
return to top
source
Imports
Init.Data.Fin.Lemmas
Init.Data.UInt.Basic
Imported by
commandDeclare_uint_theorems_
UInt8
.
le_trans
UInt8
.
one_def
UInt8
.
instInhabited
UInt8
.
lt_trans
UInt8
.
not_lt
UInt8
.
mod_def
UInt8
.
zero_def
UInt8
.
mk_val_eq
UInt8
.
add_def
UInt8
.
sub_def
UInt8
.
val_eq_of_eq
UInt8
.
ne_of_val_ne
UInt8
.
mul_def
UInt8
.
ne_of_lt
UInt8
.
mod_lt
UInt8
.
modn_lt
UInt8
.
modn_toNat
UInt8
.
le_total
UInt8
.
lt_irrefl
UInt8
.
zero_toNat
UInt8
.
div_toNat
UInt8
.
le_refl
UInt8
.
not_le
UInt8
.
val_eq_of_lt
UInt8
.
mod_toNat
UInt8
.
lt_iff_val_lt_val
UInt8
.
lt_asymm
UInt8
.
eq_of_val_eq
UInt8
.
toNat
.
inj
UInt8
.
le_def
UInt8
.
lt_def
UInt16
.
add_def
UInt16
.
le_trans
UInt16
.
val_eq_of_eq
UInt16
.
le_refl
UInt16
.
lt_iff_val_lt_val
UInt16
.
mk_val_eq
UInt16
.
le_def
UInt16
.
lt_asymm
UInt16
.
lt_irrefl
UInt16
.
not_lt
UInt16
.
zero_toNat
UInt16
.
mod_toNat
UInt16
.
one_def
UInt16
.
div_toNat
UInt16
.
lt_def
UInt16
.
zero_def
UInt16
.
not_le
UInt16
.
modn_toNat
UInt16
.
mod_def
UInt16
.
ne_of_lt
UInt16
.
le_total
UInt16
.
mod_lt
UInt16
.
mul_def
UInt16
.
instInhabited
UInt16
.
sub_def
UInt16
.
toNat
.
inj
UInt16
.
ne_of_val_ne
UInt16
.
val_eq_of_lt
UInt16
.
modn_lt
UInt16
.
eq_of_val_eq
UInt16
.
lt_trans
UInt32
.
ne_of_lt
UInt32
.
mod_def
UInt32
.
zero_toNat
UInt32
.
toNat
.
inj
UInt32
.
le_def
UInt32
.
add_def
UInt32
.
ne_of_val_ne
UInt32
.
mk_val_eq
UInt32
.
zero_def
UInt32
.
div_toNat
UInt32
.
lt_iff_val_lt_val
UInt32
.
modn_lt
UInt32
.
lt_trans
UInt32
.
mul_def
UInt32
.
eq_of_val_eq
UInt32
.
val_eq_of_lt
UInt32
.
lt_irrefl
UInt32
.
lt_asymm
UInt32
.
not_le
UInt32
.
val_eq_of_eq
UInt32
.
modn_toNat
UInt32
.
le_total
UInt32
.
one_def
UInt32
.
sub_def
UInt32
.
le_refl
UInt32
.
mod_lt
UInt32
.
le_trans
UInt32
.
lt_def
UInt32
.
not_lt
UInt32
.
mod_toNat
UInt32
.
instInhabited
UInt64
.
add_def
UInt64
.
mod_def
UInt64
.
val_eq_of_lt
UInt64
.
lt_irrefl
UInt64
.
zero_def
UInt64
.
lt_asymm
UInt64
.
le_total
UInt64
.
val_eq_of_eq
UInt64
.
le_trans
UInt64
.
lt_def
UInt64
.
lt_iff_val_lt_val
UInt64
.
sub_def
UInt64
.
mod_lt
UInt64
.
eq_of_val_eq
UInt64
.
mod_toNat
UInt64
.
not_le
UInt64
.
mul_def
UInt64
.
not_lt
UInt64
.
modn_toNat
UInt64
.
toNat
.
inj
UInt64
.
div_toNat
UInt64
.
lt_trans
UInt64
.
modn_lt
UInt64
.
ne_of_lt
UInt64
.
mk_val_eq
UInt64
.
le_def
UInt64
.
one_def
UInt64
.
instInhabited
UInt64
.
zero_toNat
UInt64
.
ne_of_val_ne
UInt64
.
le_refl
USize
.
toNat
.
inj
USize
.
mk_val_eq
USize
.
val_eq_of_lt
USize
.
lt_iff_val_lt_val
USize
.
ne_of_val_ne
USize
.
mod_lt
USize
.
zero_toNat
USize
.
modn_toNat
USize
.
div_toNat
USize
.
lt_asymm
USize
.
mod_toNat
USize
.
le_trans
USize
.
zero_def
USize
.
modn_lt
USize
.
lt_def
USize
.
ne_of_lt
USize
.
val_eq_of_eq
USize
.
sub_def
USize
.
not_lt
USize
.
le_def
USize
.
eq_of_val_eq
USize
.
one_def
USize
.
add_def
USize
.
lt_trans
USize
.
mul_def
USize
.
instInhabited
USize
.
le_refl
USize
.
mod_def
USize
.
lt_irrefl
USize
.
not_le
USize
.
le_total
source
def
commandDeclare_uint_theorems_
:
Lean.ParserDescr
Equations
One or more equations did not get rendered due to their size.
Instances For
source
theorem
UInt8
.
le_trans
{a :
UInt8
}
{b :
UInt8
}
{c :
UInt8
}
:
a
≤
b
→
b
≤
c
→
a
≤
c
source
theorem
UInt8
.
one_def
:
1
=
{
val
:=
1
}
source
instance
UInt8
.
instInhabited
:
Inhabited
UInt8
Equations
UInt8.instInhabited
=
{
default
:=
0
}
source
theorem
UInt8
.
lt_trans
{a :
UInt8
}
{b :
UInt8
}
{c :
UInt8
}
:
a
<
b
→
b
<
c
→
a
<
c
source
@[simp]
theorem
UInt8
.
not_lt
{a :
UInt8
}
{b :
UInt8
}
:
¬
a
<
b
↔
b
≤
a
source
theorem
UInt8
.
mod_def
(a :
UInt8
)
(b :
UInt8
)
:
a
%
b
=
{
val
:=
a
.val
%
b
.val
}
source
theorem
UInt8
.
zero_def
:
0
=
{
val
:=
0
}
source
@[simp]
theorem
UInt8
.
mk_val_eq
(a :
UInt8
)
:
{
val
:=
a
.val
}
=
a
source
theorem
UInt8
.
add_def
(a :
UInt8
)
(b :
UInt8
)
:
a
+
b
=
{
val
:=
a
.val
+
b
.val
}
source
theorem
UInt8
.
sub_def
(a :
UInt8
)
(b :
UInt8
)
:
a
-
b
=
{
val
:=
a
.val
-
b
.val
}
source
theorem
UInt8
.
val_eq_of_eq
{a :
UInt8
}
{b :
UInt8
}
(h :
a
=
b
)
:
a
.val
=
b
.val
source
theorem
UInt8
.
ne_of_val_ne
{a :
UInt8
}
{b :
UInt8
}
(h :
a
.val
≠
b
.val
)
:
a
≠
b
source
theorem
UInt8
.
mul_def
(a :
UInt8
)
(b :
UInt8
)
:
a
*
b
=
{
val
:=
a
.val
*
b
.val
}
source
theorem
UInt8
.
ne_of_lt
{a :
UInt8
}
{b :
UInt8
}
(h :
a
<
b
)
:
a
≠
b
source
theorem
UInt8
.
mod_lt
(a :
UInt8
)
(b :
UInt8
)
(h :
0
<
b
)
:
a
%
b
<
b
source
theorem
UInt8
.
modn_lt
{m :
Nat
}
(u :
UInt8
)
:
m
>
0
→
(
u
%
m
)
.toNat
<
m
source
@[simp]
theorem
UInt8
.
modn_toNat
(a :
UInt8
)
(b :
Nat
)
:
(
a
.modn
b
)
.toNat
=
a
.toNat
%
b
source
theorem
UInt8
.
le_total
(a :
UInt8
)
(b :
UInt8
)
:
a
≤
b
∨
b
≤
a
source
@[simp]
theorem
UInt8
.
lt_irrefl
(a :
UInt8
)
:
¬
a
<
a
source
@[simp]
theorem
UInt8
.
zero_toNat
:
UInt8.toNat
0
=
0
source
@[simp]
theorem
UInt8
.
div_toNat
(a :
UInt8
)
(b :
UInt8
)
:
(
a
/
b
)
.toNat
=
a
.toNat
/
b
.toNat
source
@[simp]
theorem
UInt8
.
le_refl
(a :
UInt8
)
:
a
≤
a
source
@[simp]
theorem
UInt8
.
not_le
{a :
UInt8
}
{b :
UInt8
}
:
¬
a
≤
b
↔
b
<
a
source
theorem
UInt8
.
val_eq_of_lt
{a :
Nat
}
:
a
<
UInt8.size
→
↑
(
UInt8.ofNat
a
)
.val
=
a
source
@[simp]
theorem
UInt8
.
mod_toNat
(a :
UInt8
)
(b :
UInt8
)
:
(
a
%
b
)
.toNat
=
a
.toNat
%
b
.toNat
source
theorem
UInt8
.
lt_iff_val_lt_val
{a :
UInt8
}
{b :
UInt8
}
:
a
<
b
↔
a
.val
<
b
.val
source
theorem
UInt8
.
lt_asymm
{a :
UInt8
}
{b :
UInt8
}
(h :
a
<
b
)
:
¬
b
<
a
source
theorem
UInt8
.
eq_of_val_eq
{a :
UInt8
}
{b :
UInt8
}
(h :
a
.val
=
b
.val
)
:
a
=
b
source
theorem
UInt8
.
toNat
.
inj
{a :
UInt8
}
{b :
UInt8
}
:
a
.toNat
=
b
.toNat
→
a
=
b
source
theorem
UInt8
.
le_def
{a :
UInt8
}
{b :
UInt8
}
:
a
≤
b
↔
a
.val
≤
b
.val
source
theorem
UInt8
.
lt_def
{a :
UInt8
}
{b :
UInt8
}
:
a
<
b
↔
a
.val
<
b
.val
source
theorem
UInt16
.
add_def
(a :
UInt16
)
(b :
UInt16
)
:
a
+
b
=
{
val
:=
a
.val
+
b
.val
}
source
theorem
UInt16
.
le_trans
{a :
UInt16
}
{b :
UInt16
}
{c :
UInt16
}
:
a
≤
b
→
b
≤
c
→
a
≤
c
source
theorem
UInt16
.
val_eq_of_eq
{a :
UInt16
}
{b :
UInt16
}
(h :
a
=
b
)
:
a
.val
=
b
.val
source
@[simp]
theorem
UInt16
.
le_refl
(a :
UInt16
)
:
a
≤
a
source
theorem
UInt16
.
lt_iff_val_lt_val
{a :
UInt16
}
{b :
UInt16
}
:
a
<
b
↔
a
.val
<
b
.val
source
@[simp]
theorem
UInt16
.
mk_val_eq
(a :
UInt16
)
:
{
val
:=
a
.val
}
=
a
source
theorem
UInt16
.
le_def
{a :
UInt16
}
{b :
UInt16
}
:
a
≤
b
↔
a
.val
≤
b
.val
source
theorem
UInt16
.
lt_asymm
{a :
UInt16
}
{b :
UInt16
}
(h :
a
<
b
)
:
¬
b
<
a
source
@[simp]
theorem
UInt16
.
lt_irrefl
(a :
UInt16
)
:
¬
a
<
a
source
@[simp]
theorem
UInt16
.
not_lt
{a :
UInt16
}
{b :
UInt16
}
:
¬
a
<
b
↔
b
≤
a
source
@[simp]
theorem
UInt16
.
zero_toNat
:
UInt16.toNat
0
=
0
source
@[simp]
theorem
UInt16
.
mod_toNat
(a :
UInt16
)
(b :
UInt16
)
:
(
a
%
b
)
.toNat
=
a
.toNat
%
b
.toNat
source
theorem
UInt16
.
one_def
:
1
=
{
val
:=
1
}
source
@[simp]
theorem
UInt16
.
div_toNat
(a :
UInt16
)
(b :
UInt16
)
:
(
a
/
b
)
.toNat
=
a
.toNat
/
b
.toNat
source
theorem
UInt16
.
lt_def
{a :
UInt16
}
{b :
UInt16
}
:
a
<
b
↔
a
.val
<
b
.val
source
theorem
UInt16
.
zero_def
:
0
=
{
val
:=
0
}
source
@[simp]
theorem
UInt16
.
not_le
{a :
UInt16
}
{b :
UInt16
}
:
¬
a
≤
b
↔
b
<
a
source
@[simp]
theorem
UInt16
.
modn_toNat
(a :
UInt16
)
(b :
Nat
)
:
(
a
.modn
b
)
.toNat
=
a
.toNat
%
b
source
theorem
UInt16
.
mod_def
(a :
UInt16
)
(b :
UInt16
)
:
a
%
b
=
{
val
:=
a
.val
%
b
.val
}
source
theorem
UInt16
.
ne_of_lt
{a :
UInt16
}
{b :
UInt16
}
(h :
a
<
b
)
:
a
≠
b
source
theorem
UInt16
.
le_total
(a :
UInt16
)
(b :
UInt16
)
:
a
≤
b
∨
b
≤
a
source
theorem
UInt16
.
mod_lt
(a :
UInt16
)
(b :
UInt16
)
(h :
0
<
b
)
:
a
%
b
<
b
source
theorem
UInt16
.
mul_def
(a :
UInt16
)
(b :
UInt16
)
:
a
*
b
=
{
val
:=
a
.val
*
b
.val
}
source
instance
UInt16
.
instInhabited
:
Inhabited
UInt16
Equations
UInt16.instInhabited
=
{
default
:=
0
}
source
theorem
UInt16
.
sub_def
(a :
UInt16
)
(b :
UInt16
)
:
a
-
b
=
{
val
:=
a
.val
-
b
.val
}
source
theorem
UInt16
.
toNat
.
inj
{a :
UInt16
}
{b :
UInt16
}
:
a
.toNat
=
b
.toNat
→
a
=
b
source
theorem
UInt16
.
ne_of_val_ne
{a :
UInt16
}
{b :
UInt16
}
(h :
a
.val
≠
b
.val
)
:
a
≠
b
source
theorem
UInt16
.
val_eq_of_lt
{a :
Nat
}
:
a
<
UInt16.size
→
↑
(
UInt16.ofNat
a
)
.val
=
a
source
theorem
UInt16
.
modn_lt
{m :
Nat
}
(u :
UInt16
)
:
m
>
0
→
(
u
%
m
)
.toNat
<
m
source
theorem
UInt16
.
eq_of_val_eq
{a :
UInt16
}
{b :
UInt16
}
(h :
a
.val
=
b
.val
)
:
a
=
b
source
theorem
UInt16
.
lt_trans
{a :
UInt16
}
{b :
UInt16
}
{c :
UInt16
}
:
a
<
b
→
b
<
c
→
a
<
c
source
theorem
UInt32
.
ne_of_lt
{a :
UInt32
}
{b :
UInt32
}
(h :
a
<
b
)
:
a
≠
b
source
theorem
UInt32
.
mod_def
(a :
UInt32
)
(b :
UInt32
)
:
a
%
b
=
{
val
:=
a
.val
%
b
.val
}
source
@[simp]
theorem
UInt32
.
zero_toNat
:
UInt32.toNat
0
=
0
source
theorem
UInt32
.
toNat
.
inj
{a :
UInt32
}
{b :
UInt32
}
:
a
.toNat
=
b
.toNat
→
a
=
b
source
theorem
UInt32
.
le_def
{a :
UInt32
}
{b :
UInt32
}
:
a
≤
b
↔
a
.val
≤
b
.val
source
theorem
UInt32
.
add_def
(a :
UInt32
)
(b :
UInt32
)
:
a
+
b
=
{
val
:=
a
.val
+
b
.val
}
source
theorem
UInt32
.
ne_of_val_ne
{a :
UInt32
}
{b :
UInt32
}
(h :
a
.val
≠
b
.val
)
:
a
≠
b
source
@[simp]
theorem
UInt32
.
mk_val_eq
(a :
UInt32
)
:
{
val
:=
a
.val
}
=
a
source
theorem
UInt32
.
zero_def
:
0
=
{
val
:=
0
}
source
@[simp]
theorem
UInt32
.
div_toNat
(a :
UInt32
)
(b :
UInt32
)
:
(
a
/
b
)
.toNat
=
a
.toNat
/
b
.toNat
source
theorem
UInt32
.
lt_iff_val_lt_val
{a :
UInt32
}
{b :
UInt32
}
:
a
<
b
↔
a
.val
<
b
.val
source
theorem
UInt32
.
modn_lt
{m :
Nat
}
(u :
UInt32
)
:
m
>
0
→
(
u
%
m
)
.toNat
<
m
source
theorem
UInt32
.
lt_trans
{a :
UInt32
}
{b :
UInt32
}
{c :
UInt32
}
:
a
<
b
→
b
<
c
→
a
<
c
source
theorem
UInt32
.
mul_def
(a :
UInt32
)
(b :
UInt32
)
:
a
*
b
=
{
val
:=
a
.val
*
b
.val
}
source
theorem
UInt32
.
eq_of_val_eq
{a :
UInt32
}
{b :
UInt32
}
(h :
a
.val
=
b
.val
)
:
a
=
b
source
theorem
UInt32
.
val_eq_of_lt
{a :
Nat
}
:
a
<
UInt32.size
→
↑
(
UInt32.ofNat
a
)
.val
=
a
source
@[simp]
theorem
UInt32
.
lt_irrefl
(a :
UInt32
)
:
¬
a
<
a
source
theorem
UInt32
.
lt_asymm
{a :
UInt32
}
{b :
UInt32
}
(h :
a
<
b
)
:
¬
b
<
a
source
@[simp]
theorem
UInt32
.
not_le
{a :
UInt32
}
{b :
UInt32
}
:
¬
a
≤
b
↔
b
<
a
source
theorem
UInt32
.
val_eq_of_eq
{a :
UInt32
}
{b :
UInt32
}
(h :
a
=
b
)
:
a
.val
=
b
.val
source
@[simp]
theorem
UInt32
.
modn_toNat
(a :
UInt32
)
(b :
Nat
)
:
(
a
.modn
b
)
.toNat
=
a
.toNat
%
b
source
theorem
UInt32
.
le_total
(a :
UInt32
)
(b :
UInt32
)
:
a
≤
b
∨
b
≤
a
source
theorem
UInt32
.
one_def
:
1
=
{
val
:=
1
}
source
theorem
UInt32
.
sub_def
(a :
UInt32
)
(b :
UInt32
)
:
a
-
b
=
{
val
:=
a
.val
-
b
.val
}
source
@[simp]
theorem
UInt32
.
le_refl
(a :
UInt32
)
:
a
≤
a
source
theorem
UInt32
.
mod_lt
(a :
UInt32
)
(b :
UInt32
)
(h :
0
<
b
)
:
a
%
b
<
b
source
theorem
UInt32
.
le_trans
{a :
UInt32
}
{b :
UInt32
}
{c :
UInt32
}
:
a
≤
b
→
b
≤
c
→
a
≤
c
source
theorem
UInt32
.
lt_def
{a :
UInt32
}
{b :
UInt32
}
:
a
<
b
↔
a
.val
<
b
.val
source
@[simp]
theorem
UInt32
.
not_lt
{a :
UInt32
}
{b :
UInt32
}
:
¬
a
<
b
↔
b
≤
a
source
@[simp]
theorem
UInt32
.
mod_toNat
(a :
UInt32
)
(b :
UInt32
)
:
(
a
%
b
)
.toNat
=
a
.toNat
%
b
.toNat
source
instance
UInt32
.
instInhabited
:
Inhabited
UInt32
Equations
UInt32.instInhabited
=
{
default
:=
0
}
source
theorem
UInt64
.
add_def
(a :
UInt64
)
(b :
UInt64
)
:
a
+
b
=
{
val
:=
a
.val
+
b
.val
}
source
theorem
UInt64
.
mod_def
(a :
UInt64
)
(b :
UInt64
)
:
a
%
b
=
{
val
:=
a
.val
%
b
.val
}
source
theorem
UInt64
.
val_eq_of_lt
{a :
Nat
}
:
a
<
UInt64.size
→
↑
(
UInt64.ofNat
a
)
.val
=
a
source
@[simp]
theorem
UInt64
.
lt_irrefl
(a :
UInt64
)
:
¬
a
<
a
source
theorem
UInt64
.
zero_def
:
0
=
{
val
:=
0
}
source
theorem
UInt64
.
lt_asymm
{a :
UInt64
}
{b :
UInt64
}
(h :
a
<
b
)
:
¬
b
<
a
source
theorem
UInt64
.
le_total
(a :
UInt64
)
(b :
UInt64
)
:
a
≤
b
∨
b
≤
a
source
theorem
UInt64
.
val_eq_of_eq
{a :
UInt64
}
{b :
UInt64
}
(h :
a
=
b
)
:
a
.val
=
b
.val
source
theorem
UInt64
.
le_trans
{a :
UInt64
}
{b :
UInt64
}
{c :
UInt64
}
:
a
≤
b
→
b
≤
c
→
a
≤
c
source
theorem
UInt64
.
lt_def
{a :
UInt64
}
{b :
UInt64
}
:
a
<
b
↔
a
.val
<
b
.val
source
theorem
UInt64
.
lt_iff_val_lt_val
{a :
UInt64
}
{b :
UInt64
}
:
a
<
b
↔
a
.val
<
b
.val
source
theorem
UInt64
.
sub_def
(a :
UInt64
)
(b :
UInt64
)
:
a
-
b
=
{
val
:=
a
.val
-
b
.val
}
source
theorem
UInt64
.
mod_lt
(a :
UInt64
)
(b :
UInt64
)
(h :
0
<
b
)
:
a
%
b
<
b
source
theorem
UInt64
.
eq_of_val_eq
{a :
UInt64
}
{b :
UInt64
}
(h :
a
.val
=
b
.val
)
:
a
=
b
source
@[simp]
theorem
UInt64
.
mod_toNat
(a :
UInt64
)
(b :
UInt64
)
:
(
a
%
b
)
.toNat
=
a
.toNat
%
b
.toNat
source
@[simp]
theorem
UInt64
.
not_le
{a :
UInt64
}
{b :
UInt64
}
:
¬
a
≤
b
↔
b
<
a
source
theorem
UInt64
.
mul_def
(a :
UInt64
)
(b :
UInt64
)
:
a
*
b
=
{
val
:=
a
.val
*
b
.val
}
source
@[simp]
theorem
UInt64
.
not_lt
{a :
UInt64
}
{b :
UInt64
}
:
¬
a
<
b
↔
b
≤
a
source
@[simp]
theorem
UInt64
.
modn_toNat
(a :
UInt64
)
(b :
Nat
)
:
(
a
.modn
b
)
.toNat
=
a
.toNat
%
b
source
theorem
UInt64
.
toNat
.
inj
{a :
UInt64
}
{b :
UInt64
}
:
a
.toNat
=
b
.toNat
→
a
=
b
source
@[simp]
theorem
UInt64
.
div_toNat
(a :
UInt64
)
(b :
UInt64
)
:
(
a
/
b
)
.toNat
=
a
.toNat
/
b
.toNat
source
theorem
UInt64
.
lt_trans
{a :
UInt64
}
{b :
UInt64
}
{c :
UInt64
}
:
a
<
b
→
b
<
c
→
a
<
c
source
theorem
UInt64
.
modn_lt
{m :
Nat
}
(u :
UInt64
)
:
m
>
0
→
(
u
%
m
)
.toNat
<
m
source
theorem
UInt64
.
ne_of_lt
{a :
UInt64
}
{b :
UInt64
}
(h :
a
<
b
)
:
a
≠
b
source
@[simp]
theorem
UInt64
.
mk_val_eq
(a :
UInt64
)
:
{
val
:=
a
.val
}
=
a
source
theorem
UInt64
.
le_def
{a :
UInt64
}
{b :
UInt64
}
:
a
≤
b
↔
a
.val
≤
b
.val
source
theorem
UInt64
.
one_def
:
1
=
{
val
:=
1
}
source
instance
UInt64
.
instInhabited
:
Inhabited
UInt64
Equations
UInt64.instInhabited
=
{
default
:=
0
}
source
@[simp]
theorem
UInt64
.
zero_toNat
:
UInt64.toNat
0
=
0
source
theorem
UInt64
.
ne_of_val_ne
{a :
UInt64
}
{b :
UInt64
}
(h :
a
.val
≠
b
.val
)
:
a
≠
b
source
@[simp]
theorem
UInt64
.
le_refl
(a :
UInt64
)
:
a
≤
a
source
theorem
USize
.
toNat
.
inj
{a :
USize
}
{b :
USize
}
:
a
.toNat
=
b
.toNat
→
a
=
b
source
@[simp]
theorem
USize
.
mk_val_eq
(a :
USize
)
:
{
val
:=
a
.val
}
=
a
source
theorem
USize
.
val_eq_of_lt
{a :
Nat
}
:
a
<
USize.size
→
↑
(
USize.ofNat
a
)
.val
=
a
source
theorem
USize
.
lt_iff_val_lt_val
{a :
USize
}
{b :
USize
}
:
a
<
b
↔
a
.val
<
b
.val
source
theorem
USize
.
ne_of_val_ne
{a :
USize
}
{b :
USize
}
(h :
a
.val
≠
b
.val
)
:
a
≠
b
source
theorem
USize
.
mod_lt
(a :
USize
)
(b :
USize
)
(h :
0
<
b
)
:
a
%
b
<
b
source
@[simp]
theorem
USize
.
zero_toNat
:
USize.toNat
0
=
0
source
@[simp]
theorem
USize
.
modn_toNat
(a :
USize
)
(b :
Nat
)
:
(
a
.modn
b
)
.toNat
=
a
.toNat
%
b
source
@[simp]
theorem
USize
.
div_toNat
(a :
USize
)
(b :
USize
)
:
(
a
/
b
)
.toNat
=
a
.toNat
/
b
.toNat
source
theorem
USize
.
lt_asymm
{a :
USize
}
{b :
USize
}
(h :
a
<
b
)
:
¬
b
<
a
source
@[simp]
theorem
USize
.
mod_toNat
(a :
USize
)
(b :
USize
)
:
(
a
%
b
)
.toNat
=
a
.toNat
%
b
.toNat
source
theorem
USize
.
le_trans
{a :
USize
}
{b :
USize
}
{c :
USize
}
:
a
≤
b
→
b
≤
c
→
a
≤
c
source
theorem
USize
.
zero_def
:
0
=
{
val
:=
0
}
source
theorem
USize
.
modn_lt
{m :
Nat
}
(u :
USize
)
:
m
>
0
→
(
u
%
m
)
.toNat
<
m
source
theorem
USize
.
lt_def
{a :
USize
}
{b :
USize
}
:
a
<
b
↔
a
.val
<
b
.val
source
theorem
USize
.
ne_of_lt
{a :
USize
}
{b :
USize
}
(h :
a
<
b
)
:
a
≠
b
source
theorem
USize
.
val_eq_of_eq
{a :
USize
}
{b :
USize
}
(h :
a
=
b
)
:
a
.val
=
b
.val
source
theorem
USize
.
sub_def
(a :
USize
)
(b :
USize
)
:
a
-
b
=
{
val
:=
a
.val
-
b
.val
}
source
@[simp]
theorem
USize
.
not_lt
{a :
USize
}
{b :
USize
}
:
¬
a
<
b
↔
b
≤
a
source
theorem
USize
.
le_def
{a :
USize
}
{b :
USize
}
:
a
≤
b
↔
a
.val
≤
b
.val
source
theorem
USize
.
eq_of_val_eq
{a :
USize
}
{b :
USize
}
(h :
a
.val
=
b
.val
)
:
a
=
b
source
theorem
USize
.
one_def
:
1
=
{
val
:=
1
}
source
theorem
USize
.
add_def
(a :
USize
)
(b :
USize
)
:
a
+
b
=
{
val
:=
a
.val
+
b
.val
}
source
theorem
USize
.
lt_trans
{a :
USize
}
{b :
USize
}
{c :
USize
}
:
a
<
b
→
b
<
c
→
a
<
c
source
theorem
USize
.
mul_def
(a :
USize
)
(b :
USize
)
:
a
*
b
=
{
val
:=
a
.val
*
b
.val
}
source
instance
USize
.
instInhabited
:
Inhabited
USize
Equations
USize.instInhabited
=
{
default
:=
0
}
source
@[simp]
theorem
USize
.
le_refl
(a :
USize
)
:
a
≤
a
source
theorem
USize
.
mod_def
(a :
USize
)
(b :
USize
)
:
a
%
b
=
{
val
:=
a
.val
%
b
.val
}
source
@[simp]
theorem
USize
.
lt_irrefl
(a :
USize
)
:
¬
a
<
a
source
@[simp]
theorem
USize
.
not_le
{a :
USize
}
{b :
USize
}
:
¬
a
≤
b
↔
b
<
a
source
theorem
USize
.
le_total
(a :
USize
)
(b :
USize
)
:
a
≤
b
∨
b
≤
a