proposition: Theorem digitLess : forall q : Z, q <> 0%Z -> (Zpower_nat n (pred (digit q)) <= Z.abs q)%Z.
proof: Proof. intros q; case q. intros H; contradict H; auto with zarith. intros p H; unfold digit in |- *; generalize (digitAuxLess (Z.abs (Zpos p)) 1 (xO p)); case (digitAux (Z.abs (Zpos p)) 1 (xO p)); simpl in |- *; intros; lia. intros p H; unfold digit in |- *; generalize (digitAuxLess (Z.abs (Zneg p)) 1 (xO p)); case (digitAux (Z.abs (Zneg p)) 1 (xO p)); simpl in |- *; intros; lia. Qed.
imports: Reals ZArith List PeanoNat Psatz