proposition: Theorem maxDiv_opp : forall (v : Z) (p : nat), maxDiv v p = maxDiv (- v) p.
proof: Proof. intros v p; elim p; simpl in |- *; auto. intros n H; case (ZdividesP v (radix * Zpower_nat radix n)); case (ZdividesP (- v) (radix * Zpower_nat radix n)); auto. intros Z1 Z2; case Z1. case Z2; intros z1 Hz1; exists (- z1)%Z; rewrite Hz1; ring. intros Z1 Z2; case Z2. case Z1; intros z1 Hz1; exists (- z1)%Z. rewrite <- (Z.opp_involutive v); rewrite Hz1; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz