Commit ad9ecfcb authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Weakened hypothesis.

parent e1f93b84
......@@ -721,13 +721,15 @@ Qed.
Lemma Zpower_gt_0 :
forall b p,
(0 < b)%Z -> (0 < p)%Z ->
(0 < b)%Z -> (0 <= p)%Z ->
(0 < Zpower b p)%Z.
Proof.
intros b p Hb Hz.
unfold Zpower.
destruct p ; try easy.
destruct p.
easy.
now apply Zpower_pos_gt_0.
now elim Hz.
Qed.
Lemma Zpower_gt_1 :
......
......@@ -61,7 +61,7 @@ simpl.
split.
apply Zpower_gt_0.
now apply Zlt_le_trans with (2 := radix_prop beta).
exact Hp.
now apply Zlt_le_weak.
apply Zle_refl.
rewrite Hx1.
eexists ; repeat split.
......
......@@ -44,7 +44,7 @@ now rewrite Rmult_0_l.
simpl.
apply Zpower_gt_0.
now apply Zlt_le_trans with (2 := radix_prop beta).
exact Hp.
now apply Zlt_le_weak.
rewrite Hx1.
eexists ; repeat split.
simpl.
......
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