proposition: Theorem digitAdd : forall (q : Z) (r : nat), q <> 0%Z -> digit (q * Zpower_nat n r) = digit q + r.
proof: Proof. intros q r H0. apply digitInv. replace (pred (digit q + r)) with (pred (digit q) + r). rewrite Zpower_nat_is_exp; rewrite Zabs_Zmult; rewrite (fun x => Z.abs_eq (Zpower_nat n x)); auto with zarith arith. apply Zmult_le_compat_r. apply digitLess; auto with zarith. apply Zpower_NR0; auto with zarith. apply Zpower_NR0; auto with zarith. generalize (digitNotZero _ H0); case (digit q); auto with arith. intros H'; contradict H'; auto with arith. rewrite Zpower_nat_is_exp; rewrite Zabs_Zmult; rewrite (fun x => Z.abs_eq (Zpower_nat n x)); auto with zarith arith. apply Zmult_lt_compat_r. apply Zpower_nat_less; auto with zarith. apply digitMore; auto with zarith. apply Zpower_NR0; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz