proposition: Theorem Zdigits_succ_le : forall x, (0 <= x)%Z -> (Zdigits (x + 1) <= Zdigits x + 1)%Z.
proof: 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.
imports: Coq(Lia ZArith Zquot) Zaux