proposition: Theorem Zdigits_gt_0 : forall n, n <> Z0 -> (0 < Zdigits n)%Z.
proof: Proof. intros n Zn. rewrite <- (Zdigits_abs n). assert (Hn: (0 < Z.abs n)%Z). destruct n ; [|easy|easy]. now elim Zn. destruct (Z.abs n) as [|p|p] ; try easy ; clear. simpl. generalize 1%Z (radix_val beta) (refl_equal Lt : (0 < 1)%Z). induction (digits2_Pnat p). easy. simpl. intros. case Zlt_bool. exact H. apply IHn. now apply Zlt_lt_succ. Qed.
imports: Coq(Lia ZArith Zquot) Zaux