Commit c3caf4b6 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Weakened hypothesis of Zpower_gt_0.

parent 4d4f22a0
......@@ -553,7 +553,8 @@ ring.
omega.
assert (Hp: (Zpower beta k > 0)%Z).
apply Zlt_gt.
now apply Zpower_gt_0.
apply Zpower_gt_0.
now apply Zlt_le_weak.
(* . *)
rewrite 2!Hr.
rewrite Zmult_plus_distr_l, Zmult_1_l.
......
......@@ -114,7 +114,8 @@ apply generic_format_0.
exists (Float beta 0 0).
split.
now rewrite F2R_0.
now apply Zpower_gt_0.
apply Zpower_gt_0.
now apply Zlt_le_weak.
(* . *)
destruct (ln_beta beta x) as (ex, Hx2).
simpl.
......
......@@ -2150,13 +2150,14 @@ Qed.
Theorem Zpower_gt_0 :
forall p,
(0 < p)%Z ->
(0 <= p)%Z ->
(0 < Zpower r p)%Z.
Proof.
intros.
apply Zlt_trans with 1%Z.
easy.
now apply Zpower_gt_1.
apply lt_Z2R.
rewrite Z2R_Zpower.
apply bpow_gt_0.
exact H.
Qed.
Theorem Zpower_ge_0 :
......
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