proposition: Theorem maxDivSimplAux : forall (v : Z) (p q : nat), p = maxDiv v (S (q + p)) -> p = maxDiv v (S p).
proof: Proof. intros v p q; elim q. simpl in |- *; case (ZdividesP v (radix * Zpower_nat radix p)); auto. intros n H' H'0. apply H'; auto; clear H'. simpl in H'0; generalize H'0; clear H'0. case (ZdividesP v (radix * (radix * Zpower_nat radix (n + p)))). 2: simpl in |- *; auto. intros H' H'0; contradict H'0; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz