proposition: Theorem maxDivUniqueInverse : forall (v : Z) (p : nat), Zdivides v (Zpower_nat radix p) -> ~ Zdivides v (Zpower_nat radix (S p)) -> p = maxDiv v (S p).
proof: Proof. intros v p H' H'0; simpl in |- *. case (ZdividesP v (radix * Zpower_nat radix p)); auto. intros H'1; case H'0; simpl in |- *; auto. intros H'1. generalize H'; case p; simpl in |- *; auto. intros n H'2; case (ZdividesP v (radix * Zpower_nat radix n)); auto. intros H'3; case H'3; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz