Require Export ZArith.
Require Export ZArithRing.
Require Export Omega.
Require Export Zcomplements.
Lemma A2: (a, b, c, d : Z) (Zle c a) -> (Zle d b) -> (Zle ZERO c) ->
(Zle
ZERO d) -> (Zle (Zmult
c
d)
(Zmult
a
b)).
Lemma Zle_mult': (x,y:Z)`0 < x `->`0 <= y`->`0 <= y*x`.
Lemma Zmult_le' : (x,y:Z)`0 < x`->`0 <= y*x`->`0 <= y`.
Lemma Zmult_lt' : (x,y:Z)`0 < x`->`0 < y*x`->`0 < y`.
Lemma A1: (a, b : Z) (Zlt ZERO a) -> (Zlt ZERO b) -> (Zlt ZERO (Zmult a b)).
Lemma L4: (a, b, c : Z) (Zlt ZERO c) -> (Zle (Zmult b c) (Zmult a c)) -> (Zle b a).
Lemma L5: (a, b, c : Z) (Zlt ZERO c) -> (Zlt (Zmult b c) (Zmult a c)) -> (Zlt b
a).
Lemma L6: (a, b, c, d : Z) (Zlt a b) -> (Zle c d) -> (Zlt (Zplus a c) (Zplus
b d)).
Lemma Zgt_not_le' : (n,m:Z)`m < n`->~`n <= m`.
Lemma L7: (x, y : Z) (Zle ZERO x) -> (Zle ZERO y) ->
(Zlt (Zmult y y) (Zmult
x x)) -> (Zlt y x).
Lemma L4': (a, b, c : Z) (Zlt ZERO c) -> (Zlt (Zmult a c) (Zmult b c)) -> (Zlt
a
b).
Lemma Z0lt_le_pred : (y:Z) `0 < y` -> `0 <= (Zpred y)`.
Lemma Zlt_Zmult_right : (x,y,z:Z)`0<z` -> `x < y` -> `x*z < y*z`.
Lemma Zlt_Zmult_left : (x,y,z:Z)`0<z` -> `x < y` -> `z*x < z*y`.
Lemma Zle_Zmult_right2': (x,y,z:Z)`0 <z`->`x*z <= y*z`->`x <= y`.
Lemma Zlt_Zmult_right2': (x,y,z:Z)`0 <z`->`x*z < y*z`->`x < y`.
Lemma Zgt_S_le': (n,p:Z)`n < (Zs p)`->`n <= p`.
Lemma Zle_Zmult_right'
: (x,y,z:Z)`0 < z`->`x <= y`->`x*z <= y*z`.
Lemma Z_lt_le_dec: (x,y:Z){`x < y`}+{`y <= x`}.
Lemma Zmult_reg_left'
: (x,y,z:Z)`0 <z `->`z*x = z*y`->`x = y`.
Lemma Zle_mult_simpl': (a,b,c:Z)`0 < c`->`a*c <= b*c`->`a <= b`.
Lemma Z_le_lt_dec
: (x,y:Z){`y <= x`}+{`x < y`}.
Lemma Zlt_left_plus : (a,b,c:Z)`0<=b`->`a+b<c`->`a<c`.
Lemma Zle_lt_1 : (x,y:Z)`x<y`->`x+1<=y`.