Library Coq.ZArith.auxiliary
Binary Integers (Pierre Crégut, CNET, Lannion, France)
Require
Export
Arith_base
.
Require
Import
BinInt
.
Require
Import
Zorder
.
Require
Import
Decidable
.
Require
Import
Peano_dec
.
Require
Export
Compare_dec
.
Local
Open
Scope
Z_scope
.
Moving terms from one side to the other of an inequality
Theorem
Zne_left
n
m
:
Zne
n
m
->
Zne
(
n
+
-
m
) 0.
Theorem
Zegal_left
n
m
:
n
=
m
->
n
+
-
m
=
0.
Theorem
Zle_left
n
m
:
n
<=
m
-> 0
<=
m
+
-
n
.
Theorem
Zle_left_rev
n
m
: 0
<=
m
+
-
n
->
n
<=
m
.
Theorem
Zlt_left_rev
n
m
: 0
<
m
+
-
n
->
n
<
m
.
Theorem
Zlt_left_lt
n
m
:
n
<
m
-> 0
<
m
+
-
n
.
Theorem
Zlt_left
n
m
:
n
<
m
-> 0
<=
m
+
-1
+
-
n
.
Theorem
Zge_left
n
m
:
n
>=
m
-> 0
<=
n
+
-
m
.
Theorem
Zgt_left
n
m
:
n
>
m
-> 0
<=
n
+
-1
+
-
m
.
Theorem
Zgt_left_gt
n
m
:
n
>
m
->
n
+
-
m
>
0.
Theorem
Zgt_left_rev
n
m
:
n
+
-
m
>
0 ->
n
>
m
.
Theorem
Zle_mult_approx
n
m
p
:
n
>
0 ->
p
>
0 -> 0
<=
m
-> 0
<=
m
*
n
+
p
.
Theorem
Zmult_le_approx
n
m
p
:
n
>
0 ->
n
>
p
-> 0
<=
m
*
n
+
p
-> 0
<=
m
.