Section More_Nexp.
Variable R : COrdField.
Lemma nexp_resp_ap_zero : forall (x : R) n, x [#] 0 -> x[^]n [#] 0.
Lemma nexp_distr_div : forall (x y : R) n y_ yn_, (x[/] y[//]y_) [^]n [=] (x[^]n[/] y[^]n[//]yn_).
Lemma nexp_distr_div' : forall (x y : R) n y_,
(x[/] y[//]y_) [^]n [=] (x[^]n[/] y[^]n[//]nexp_resp_ap_zero y n y_).
Lemma small_nexp_resp_lt : forall (x : R) m n,
0 [<] x -> x [<] 1 -> m < n -> x[^]n [<] x[^]m.
Lemma great_nexp_resp_lt : forall (x : R) m n, 1 [<] x -> m < n -> x[^]m [<] x[^]n.
Lemma small_nexp_resp_le : forall (x : R) m n,
0 [<=] x -> x [<=] 1 -> m <= n -> x[^]n [<=] x[^]m.
Lemma great_nexp_resp_le : forall (x : R) m n, 1 [<=] x -> m <= n -> x[^]m [<=] x[^]n.
Lemma nexp_resp_leEq : forall (x y : R) k, 0 [<=] x -> x [<=] y -> x[^]k [<=] y[^]k.
Lemma nexp_resp_leEq_one : forall c : R, 0 [<=] c -> c [<=] 1 -> forall n, c[^]n [<=] 1.
Lemma nexp_resp_leEq_neg_even : forall n, even n ->
forall x y : R, y [<=] 0 -> x [<=] y -> y[^]n [<=] x[^]n.
Lemma nexp_resp_leEq_neg_odd : forall n, odd n ->
forall x y : R, y [<=] 0 -> x [<=] y -> x[^]n [<=] y[^]n.
Lemma nexp_distr_recip : forall (x : R) n x_ xn_, (1[/] x[//]x_) [^]n [=] (1[/] x[^]n[//]xn_).
Lemma nexp_even_nonneg : forall n, even n -> forall x : R, 0 [<=] x[^]n.
Lemma nexp_resp_le' : forall c : R, 0 [<=] c -> c [<=] 1 -> forall m n, m <= n -> c[^]n [<=] c[^]m.
Lemma nexp_resp_le : forall c : R, 1 [<=] c -> forall m n, m <= n -> c[^]m [<=] c[^]n.
Lemma bin_less_un : forall n H H1, (1[/] (2:R) [^]S n[//]H) [<] (1[/] nring (S n) [//]H1).
End More_Nexp.
It would be nicer to define zexp using caseZdiff, but we already
have most properties now.
Definition zexp (x : R) x_ (n : Z) : R :=
match n with
| Z0 => 1:R
| Zpos p => x[^]nat_of_P p
| Zneg p => (1[/] x[//]x_) [^]nat_of_P p
end.
End Zexp_def.
Notation "( x ‡ Hx ) ^ n" := (zexp x Hx n) (at level 0).
Section Zexp_properties.
Variable R : COrdField.
Lemma zexp_zero : forall (x : R) x_, (x[//]x_) [^^] (0) [=] 1.
Lemma zexp_nexp : forall (x : R) x_ (n : N), (x[//]x_) [^^] (n) [=] x[^]n.
Lemma zexp_inv_nexp : forall (x : R) x_ (n : N), (x[//]x_) [^^] (- n) [=] (1[/] x[//]x_) [^]n.
Lemma zexp_inv_nexp' : forall (x : R) (n : N) x_ xn_, (x[//]x_) [^^] (- n) [=] (1[/] x[^]n[//]xn_).
Lemma zexp_strext : forall (x y : R) m x_ y_, (x[//]x_) [^^] (m) [#] (y[//]y_) [^^] (m) -> x [#] y.
Lemma zexp_wd : forall (x y : R) m x_ y_, x [=] y -> (x[//]x_) [^^] (m) [=] (y[//]y_) [^^] (m).
Lemma zexp_plus1 : forall (x : R) x_ m, (x[//]x_) [^^] (m + 1) [=] (x[//]x_) [^^] (m) [*]x.
Lemma zexp_resp_ap_zero : forall (x : R) m x_, (x[//]x_) [^^] (m) [#] 0.
Lemma zexp_inv : forall (x : R) x_ m xm_, (x[//]x_) [^^] (- m) [=] (1[/] (x[//]x_) [^^] (m) [//]xm_).
Lemma zexp_inv1 : forall (x : R) x_ m, (x[//]x_) [^^] (m - 1) [=] ((x[//]x_) [^^] (m) [/] x[//]x_).
Lemma zexp_plus : forall (x : R) x_ m n, (x[//]x_) [^^] (m + n) [=] (x[//]x_) [^^] (m) [*] (x[//]x_) [^^] (n).
Lemma zexp_minus : forall (x : R) x_ m n xn_,
(x[//]x_) [^^] (m - n) [=] ((x[//]x_) [^^] (m) [/] (x[//]x_) [^^] (n) [//]xn_).
Lemma one_zexp : forall z, (1[//]ring_non_triv _) [^^] (z) [=] (1:R).
Lemma mult_zexp : forall (x y : R) z x_ y_ xy_,
(x[*]y[//]xy_) [^^] (z) [=] (x[//]x_) [^^] (z) [*] (y[//]y_) [^^] (z).
Lemma zexp_mult : forall (x : R) m n x_ xm_,
(x[//]x_) [^^] (m * n) [=] ((x[//]x_) [^^] (m) [//]xm_) [^^] (n).
Lemma zexp_two : forall (x : R) x_, (x[//]x_) [^^] (2) [=] x[*]x.
Lemma inv_zexp_even : forall (x : R) m, Zeven m -> forall x_ x__,
([--]x[//]x__) [^^] (m) [=] (x[//]x_) [^^] (m).
Lemma inv_zexp_two : forall (x : R) x_ x__, ([--]x[//]x__) [^^] (2) [=] (x[//]x_) [^^] (2).
Lemma inv_zexp_odd : forall (x : R) m, Zodd m -> forall x_ x__,
([--]x[//]x__) [^^] (m) [=] [--] (x[//]x_) [^^] (m).
Lemma zexp_one : forall (x : R) x_, (x[//]x_) [^^] (1) [=] x.
Lemma zexp_funny : forall (x y : R) x_ y_, (x[+]y) [*] (x[-]y) [=] (x[//]x_) [^^] (2) [-] (y[//]y_) [^^] (2).
Lemma zexp_funny' : forall (x y : R) x_ y_, (x[-]y) [*] (x[+]y) [=] (x[//]x_) [^^] (2) [-] (y[//]y_) [^^] (2).
Lemma zexp_pos : forall (x : R) x_ z, 0 [<] x -> 0 [<] (x[//]x_) [^^] (z).
End Zexp_properties.
Section Root_Unique.
Variable R : COrdField.
Lemma root_unique : forall x y : R,
0 [<=] x -> 0 [<=] y -> forall n, 0 < n -> x[^]n [=] y[^]n -> x [=] y.
Lemma root_one : forall x : R, 0 [<=] x -> forall n, 0 < n -> x[^]n [=] 1 -> x [=] 1.
End Root_Unique.