Require Export Zextensions.
Require Export Gomega.
Definition Zsquare := [x : ?] (Zmult x x).
Lemma Zminus_Zsquare:
(A, B : Z)
<Z>
(Zsquare (Zminus A B)) =
(Zminus (Zplus (Zsquare A) (Zsquare B)) (Zmult (Zmult (POS (xO xH)) A) B)).
Lemma Zplus_Zsquare:
(A, B : Z)
<Z>
(Zsquare (Zplus A B)) =
(Zplus (Zplus (Zsquare A) (Zsquare B)) (Zmult (Zmult (POS (xO xH)) A) B)).
Lemma Zmult_Zsquare:
(x, y : Z) (Zsquare (Zmult x y)) = (Zmult (Zsquare x) (Zsquare y)).
Lemma Zsquare_order:
(x, y : Z)
(Zle ZERO x) -> (Zle ZERO y) -> (Zlt (Zsquare x) (Zsquare y)) -> (Zlt x y).
Lemma Zsquare_monotonous:
(A, B : Z)
(Zle ZERO A) -> (Zle ZERO B) -> (Zle A B) -> (Zle (Zsquare A) (Zsquare B)).
Lemma thm_Zsquare:
(A, B : Z)
(Zle ZERO B) /\ (Zle B A) -> (Zle ZERO (Zminus (Zsquare A) (Zsquare B))).
Lemma thm_Zsquare2:
(A, B : Z)
(Zlt ZERO A) -> (Zlt ZERO B) -> (Zle (Zsquare A) (Zsquare B)) -> (Zle A B).
Fixpoint pow[z : Z; n : nat] : Z :=
Cases n of O => (POS xH)
| (S p) => (Zmult z (pow z p)) end.
Lemma pow_sum:
(z : Z) (h, l : nat) (pow z (plus h l)) = (Zmult (pow z h) (pow z l)).
Lemma pow_mult:
(A, B : Z)
(n : nat) <Z> (Zmult ((pow A) n) ((pow B) n)) = ((pow (Zmult A B)) n).
Lemma square_pow:
(b : Z) (h : nat) (Zsquare (pow b h)) = (pow b (mult (S (S O)) h)).
Lemma pow_pos: (x : Z) (Zlt ZERO x) -> (n : nat) (Zlt ZERO (pow x n)).
Hints Resolve pow_pos :sqrt.
Lemma pow_monotonous:
(b : Z) (Zlt ZERO b) -> (h, l : nat) (le h l) -> (Zle (pow b h) (pow b l)).