From f94725d7172b334f99ba1d546d9173828a85066d Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 21 Dec 2010 21:09:22 +0000 Subject: [PATCH] Added digits_gt_0. --- src/Calc/Fcalc_digits.v | 21 ++++++++++++++------- 1 file changed, 14 insertions(+), 7 deletions(-) diff --git a/src/Calc/Fcalc_digits.v b/src/Calc/Fcalc_digits.v index 9da16f9..02f04b1 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. -- GitLab