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.