Commit f94725d7 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Added digits_gt_0.

parent 2a3675a5
......@@ -191,16 +191,13 @@ now apply Zpower_NR0.
apply Zmult_1_r.
Qed.
Theorem digits_ge_0 :
forall n, (0 <= digits n)%Z.
Theorem digits_gt_0 :
forall n, (n <> 0)%Z -> (0 < digits n)%Z.
Proof.
intros n.
destruct (Z_eq_dec n 0) as [H|H].
now rewrite H.
intros n H.
rewrite digits_ln_beta with (1 := H).
destruct ln_beta as (e, He). simpl.
apply (le_bpow beta).
apply Rlt_le.
apply (lt_bpow beta).
apply Rle_lt_trans with (Rabs (Z2R n)).
simpl.
rewrite <- Z2R_abs.
......@@ -214,6 +211,16 @@ apply He.
now apply (Z2R_neq _ 0).
Qed.
Theorem digits_ge_0 :
forall n, (0 <= digits n)%Z.
Proof.
intros n.
destruct (Z_eq_dec n 0) as [H|H].
now rewrite H.
apply Zlt_le_weak.
now apply digits_gt_0.
Qed.
Theorem ln_beta_F2R_digits :
forall m e, m <> Z0 ->
(ln_beta beta (F2R (Float beta m e)) = digits m + e :> Z)%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