proposition: Theorem digitMore : forall q : Z, (Z.abs q < Zpower_nat n (digit q))%Z.
proof: Proof. intros q; case q. easy. intros q'; rewrite <- (Zmult_1_r (Zpower_nat n (digit (Zpos q')))). unfold digit in |- *; apply digitAuxMore; auto with zarith. rewrite Zmult_1_r. simpl in |- *; apply pos_length_pow. intros q'; rewrite <- (Zmult_1_r (Zpower_nat n (digit (Zneg q')))). unfold digit in |- *; apply digitAuxMore; auto with zarith. rewrite Zmult_1_r. simpl in |- *; apply pos_length_pow. Qed.
imports: Reals ZArith List PeanoNat Psatz