Commit 85ea4d1e authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Made Zpower_gt_0 more useful.

parent 5bf01a31
......@@ -484,10 +484,7 @@ ring.
omega.
assert (Hp: (Zpower (radix_val beta) k > 0)%Z).
apply Zlt_gt.
apply Zpower_gt_0.
generalize (radix_prop beta).
omega.
now apply Zlt_le_weak.
now apply Zpower_gt_0.
(* . *)
rewrite 2!Hr.
rewrite Zmult_plus_distr_l, Zmult_1_l.
......
......@@ -66,10 +66,7 @@ omega.
split.
apply Zmult_lt_0_compat.
exact Hm1.
apply Zpower_gt_0.
generalize (radix_prop beta).
omega.
easy.
now apply Zpower_gt_0.
rewrite digits_shift.
rewrite Zplus_comm.
apply Zle_refl.
......
......@@ -199,10 +199,7 @@ now apply Zlt_not_eq.
easy.
apply Zmult_lt_0_compat.
exact Hm.
apply Zpower_gt_0.
generalize (radix_prop beta).
omega.
easy.
now apply Zpower_gt_0.
now elim He2.
clearbody m'.
destruct Hs as (Hs1, (Hs2, Hs3)).
......
......@@ -96,9 +96,7 @@ apply generic_format_0.
exists (Float beta 0 0).
split.
now rewrite F2R_0.
apply Zpower_gt_0.
now apply Zlt_le_trans with (2 := radix_prop beta).
now apply Zlt_le_weak.
now apply Zpower_gt_0.
(* . *)
destruct (ln_beta beta x) as (ex, Hx2).
simpl.
......
......@@ -1393,19 +1393,6 @@ apply powerRZ_lt.
now apply (Z2R_lt 0).
Qed.
Theorem Zpower_gt_0 :
forall b p,
(0 < b)%Z -> (0 <= p)%Z ->
(0 < Zpower b p)%Z.
Proof.
intros b p Hb Hz.
unfold Zpower.
destruct p.
easy.
now apply Zpower_pos_gt_0.
now elim Hz.
Qed.
Theorem Zpower_gt_1 :
forall p,
(0 < p)%Z ->
......@@ -1418,6 +1405,17 @@ now apply -> (bpow_lt 0).
now apply Zlt_le_weak.
Qed.
Theorem Zpower_gt_0 :
forall p,
(0 < p)%Z ->
(0 < Zpower (radix_val r) p)%Z.
Proof.
intros.
apply Zlt_trans with 1%Z.
easy.
now apply Zpower_gt_1.
Qed.
Theorem Zpower_Zpower_nat :
forall b e, (0 <= e)%Z ->
Zpower b e = Zpower_nat b (Zabs_nat e).
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment