proposition: Theorem maxDivSimplInv : forall (v : Z) (p q : nat), p < q -> p = maxDiv v (S p) -> p = maxDiv v q.
proof: Proof. intros v p q H' H'0. replace q with (S (q - S p + p)); auto with zarith. apply maxDivSimplInvAux; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz