proposition: Theorem Zdigit_scale : forall n k k', (0 <= k')%Z -> Zdigit (Zscale n k) k' = Zdigit n (k' - k).
proof: Proof. intros n k k' Hk'. unfold Zscale. case Zle_bool_spec ; intros Hk. now apply Zdigit_mul_pow. apply Zdigit_div_pow with (1 := Hk'). lia. Qed.
imports: Coq(Lia ZArith Zquot) Zaux