proposition: Theorem Zdigits_correct : forall n, (Zpower beta (Zdigits n - 1) <= Z.abs n < Zpower beta (Zdigits n))%Z.
proof: Proof. cut (forall p, Zpower beta (Zdigits (Zpos p) - 1) <= Zpos p < Zpower beta (Zdigits (Zpos p)))%Z. intros H [|n|n] ; try exact (H n). now split. intros n. simpl. assert (U: (Zpos n < Zpower beta (Z_of_nat (S (digits2_Pnat n))))%Z). apply Z.lt_le_trans with (1 := proj2 (digits2_Pnat_correct n)). rewrite Zpower_Zpower_nat. rewrite Zabs_nat_Z_of_nat. induction (S (digits2_Pnat n)). easy. rewrite 2!(Zpower_nat_S). apply Zmult_le_compat with (2 := IHn0). apply Zle_bool_imp_le. apply beta. easy. rewrite <- (Zabs_nat_Z_of_nat n0). rewrite <- Zpower_Zpower_nat. apply (Zpower_ge_0 (Build_radix 2 (refl_equal true))). apply Zle_0_nat. apply Zle_0_nat. revert U. rewrite inj_S. unfold Z.succ. generalize (digits2_Pnat n). intros u U. pattern (radix_val beta) at 2 4 ; replace (radix_val beta) with (Zpower beta 1) by apply Zmult_1_r. assert (V: (Zpower beta (1 - 1) <= Zpos n)%Z). now apply (Zlt_le_succ 0). generalize (conj V U). clear. generalize (Z.le_refl 1). generalize 1%Z at 2 3 5 6 7 9 10. induction u. easy. rewrite inj_S; unfold Z.succ. simpl Zdigits_aux. intros v Hv U. case Zlt_bool_spec ; intros K. now split. pattern (radix_val beta) at 2 5 ; replace (radix_val beta) with (Zpower beta 1) by apply Zmult_1_r. rewrite <- Zpower_plus. rewrite Zplus_comm. apply IHu. clear -Hv ; lia. split. now ring_simplify (1 + v - 1)%Z. now rewrite Zplus_assoc. easy. apply Zle_succ_le with (1 := Hv). Qed.
imports: Coq(Lia ZArith Zquot) Zaux