diff --git a/src/Calc/Fcalc_digits.v b/src/Calc/Fcalc_digits.v index 9da16f95459c80cfec9ce48e8c1726f6e0b8a5c9..02f04b1ba8925b81a06dc527c4837881bbe661b0 100644 --- a/src/Calc/Fcalc_digits.v +++ b/src/Calc/Fcalc_digits.v @@ -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.