proposition: Theorem Zsum_digit_digit : forall n k, Zsum_digit (Zdigit n) k = Z.rem n (Zpower beta (Z_of_nat k)).
proof: Proof. intros n. induction k. apply sym_eq. apply Z.rem_1_r. simpl Zsum_digit. rewrite IHk. unfold Zdigit. rewrite <- ZOdiv_mod_mult. rewrite <- (ZOmod_mod_mult n beta). rewrite Zmult_comm. replace (beta ^ Z_of_nat k * beta)%Z with (Zpower beta (Z_of_nat (S k))). rewrite Zplus_comm, Zmult_comm. apply sym_eq. apply Z.quot_rem'. rewrite inj_S. rewrite <- (Zmult_1_r beta) at 3. apply Zpower_plus. apply Zle_0_nat. easy. Qed.
imports: Coq(Lia ZArith Zquot) Zaux