diff options
Diffstat (limited to 'flocq/Core/Digits.v')
| -rw-r--r-- | flocq/Core/Digits.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/flocq/Core/Digits.v b/flocq/Core/Digits.v index b491b436..7fe51cca 100644 --- a/flocq/Core/Digits.v +++ b/flocq/Core/Digits.v @@ -1115,6 +1115,17 @@ exact Hm. now rewrite <- (Z.abs_eq m) at 1. Qed. +Theorem Zdigits_succ_le : + forall x, (0 <= x)%Z -> + (Zdigits (x + 1) <= Zdigits x + 1)%Z. +Proof. + destruct x as [| p | p]; [intros _; now simpl | intros _ | lia]. + transitivity (Zdigits (Z.pos p * beta ^ 1)); + [apply Zdigits_le; [lia |] | rewrite Zdigits_mult_Zpower; lia]. + apply Ztac.Zlt_le_add_1. rewrite <-Z.mul_1_r at 1. apply Zmult_lt_compat_l; [lia |]. + rewrite Z.pow_1_r. apply radix_gt_1. +Qed. + End Fcore_digits. (** Specialized version for computing the number of bits of an integer *) |