proposition: Theorem maxDivUniqueDigit : forall v : Z, v <> 0 -> Zdivides v (Zpower_nat radix (maxDiv v (digit radix v))) /\ ~ Zdivides v (Zpower_nat radix (S (maxDiv v (digit radix v)))).
proof: Proof. intros v H'. apply maxDivUnique; auto. apply maxDivSimpl with (q := digit radix v); auto. apply maxDivLt; auto. apply NotDividesDigit; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz