proposition: Theorem digitAux1 : forall p r, (Zpower_nat n (S p) * r)%Z = (Zpower_nat n p * (n * r))%Z.
proof: Proof. intros p r; replace (S p) with (1 + p); [ rewrite Zpower_nat_is_exp | auto with arith ]. rewrite Zpower_nat_1; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz