proposition: Theorem maxDivCorrect : forall (v : Z) (p : nat), Zdivides v (Zpower_nat radix (maxDiv v p)).
proof: Proof. intros v p; elim p. unfold maxDiv in |- *; rewrite Zpower_nat_O; auto. apply Zdivides1. simpl in |- *. intros n H'; case (ZdividesP v (radix * Zpower_nat radix n)); simpl in |- *; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz