proposition: Theorem maxDivSimplInvAux : forall (v : Z) (p q : nat), p = maxDiv v (S p) -> p = maxDiv v (S (q + p)).
proof: Proof. intros v p q H'; elim q. simpl in |- *; auto. intros n; simpl in |- *. case (ZdividesP v (radix * Zpower_nat radix (n + p))); auto. case (ZdividesP v (radix * (radix * Zpower_nat radix (n + p)))); auto. intros H'0 H'1 H'2; contradict H'2; auto with zarith. case (ZdividesP v (radix * (radix * Zpower_nat radix (n + p)))); auto. intros H'0 H'1 H'2; case H'1. case H'0; intros z1 Hz1; exists (radix * z1)%Z;rewrite Hz1. unfold Zpower_nat; simpl; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz