proposition: Theorem maxDivLt : forall (v : Z) (p : nat), ~ Zdivides v (Zpower_nat radix p) -> maxDiv v p < p.
proof: Proof. intros v p; case p; simpl in |- *; auto. intros H'; case H'. apply Zdivides1. intros n H'; case (ZdividesP v (radix * Zpower_nat radix n)); auto. intros H'0; case H'; auto. intros H'0; generalize (maxDivLess v n); auto with arith. Qed.
imports: Reals ZArith List PeanoNat Psatz