proposition: Theorem Zdigit_digits : forall n, n <> Z0 -> Zdigit n (Zdigits n - 1) <> Z0.
proof: Proof. intros n Zn. apply Zdigit_not_0. apply Zlt_0_le_0_pred. now apply Zdigits_gt_0. ring_simplify (Zdigits n - 1 + 1)%Z. apply Zdigits_correct. Qed.
imports: Coq(Lia ZArith Zquot) Zaux