proposition: Theorem maxDivLess : forall (v : Z) (p : nat), maxDiv v p <= p.
proof: Proof. intros v p; elim p; simpl in |- *; auto. intros n H'; case (ZdividesP v (radix * Zpower_nat radix n)); auto. Qed.
imports: Reals ZArith List PeanoNat Psatz