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

Added lemma Z2R_Zpower_nat.

parent 58e8dca9
......@@ -147,13 +147,10 @@ rewrite inj_S.
omega.
apply <- bpow_lt.
apply Rle_lt_trans with (1 := proj1 He).
apply Rlt_le_trans with (Z2R (Zpower_nat 2 (S (digits2_Pnat p)))).
rewrite <- Z2R_Zpower_nat.
apply Z2R_lt.
apply Zlt_le_trans with (Zpower_nat 2 (S (digits2_Pnat p))).
exact (proj2 (digits2_Pnat_correct p)).
rewrite <- Z2R_Zpower.
apply Z2R_le.
rewrite Zpower_Zpower_nat.
rewrite Zabs_nat_Z_of_nat.
clear.
induction (S (digits2_Pnat p)).
easy.
......@@ -162,8 +159,6 @@ apply Zmult_le_compat ; try easy.
apply Zle_bool_imp_le.
apply beta.
now apply Zpower_NR0.
apply Zle_0_nat.
apply Zle_0_nat.
apply Zmult_1_r.
Qed.
......
......@@ -1128,6 +1128,17 @@ generalize (bpow_gt_0 (Zpos p)).
simpl; auto with real.
Qed.
Theorem Z2R_Zpower_nat :
forall e : nat,
Z2R (Zpower_nat (radix_val r) e) = bpow (Z_of_nat e).
Proof.
intros [|e].
split.
rewrite <- nat_of_P_o_P_of_succ_nat_eq_succ.
rewrite <- Zpower_pos_nat.
now rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P.
Qed.
Theorem Z2R_Zpower :
forall e : Z,
(0 <= e)%Z ->
......
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