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