Library Coq.ZArith.auxiliary
Binary Integers (Pierre Crégut, CNET, Lannion, France)
Moving terms from one side to the other of an inequality
Theorem Zne_left :
forall n m:
Z,
Zne n m ->
Zne (
n + - m) 0.
Theorem Zegal_left :
forall n m:
Z,
n = m ->
n + - m = 0.
Theorem Zle_left :
forall n m:
Z,
n <= m -> 0
<= m + - n.
Theorem Zle_left_rev :
forall n m:
Z, 0
<= m + - n ->
n <= m.
Theorem Zlt_left_rev :
forall n m:
Z, 0
< m + - n ->
n < m.
Theorem Zlt_left :
forall n m:
Z,
n < m -> 0
<= m + -1
+ - n.
Theorem Zlt_left_lt :
forall n m:
Z,
n < m -> 0
< m + - n.
Theorem Zge_left :
forall n m:
Z,
n >= m -> 0
<= n + - m.
Theorem Zgt_left :
forall n m:
Z,
n > m -> 0
<= n + -1
+ - m.
Theorem Zgt_left_gt :
forall n m:
Z,
n > m ->
n + - m > 0.
Theorem Zgt_left_rev :
forall n m:
Z,
n + - m > 0 ->
n > m.
Theorem Zle_mult_approx :
forall n m p:
Z,
n > 0 ->
p > 0 -> 0
<= m -> 0
<= m * n + p.
Theorem Zmult_le_approx :
forall n m p:
Z,
n > 0 ->
n > p -> 0
<= m * n + p -> 0
<= m.