proposition: Theorem maxDiv_abs : forall (v : Z) (p : nat), maxDiv v p = maxDiv (Z.abs 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 (Z.abs v) (radix * Zpower_nat radix n)); auto. intros Z1 Z2; case Z1. case Z2; intros z1 Hz1; exists (Z.abs z1); rewrite Hz1. rewrite Zabs_Zmult; f_equal. apply Z.abs_eq. apply Z.mul_nonneg_nonneg; try auto with zarith. apply Zpower_NR0; auto with zarith. intros Z1 Z2; case Z2. case Z1; intros z1 Hz1. case (Zle_or_lt v 0); intros Z4. exists (- z1)%Z; rewrite <- (Z.opp_involutive v); rewrite <- (Zabs_eq_opp v); auto; rewrite Hz1; ring. exists z1; rewrite <- (Z.abs_eq v); auto with zarith; rewrite Hz1; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz