proposition: Theorem maxDivPlus : forall (v : Z) (n : nat), v <> 0 -> maxDiv (v * Zpower_nat radix n) (digit radix v + n) = maxDiv v (digit radix v) + n.
proof: Proof. intros v n H. replace (digit radix v + n) with (digit radix (v * Zpower_nat radix n)); auto. apply sym_equal. apply maxDivUniqueInverseDigit; auto. red in |- *; intros Z1; case (Zmult_integral _ _ Z1); intros Z2. case H; auto. absurd (0 < Zpower_nat radix n)%Z; auto with zarith. now apply Zpower_nat_less. rewrite Zpower_nat_is_exp. repeat rewrite (fun x : Z => Zmult_comm x (Zpower_nat radix n)). apply ZdividesMult; auto. case (maxDivUniqueDigit v); auto. replace (S (maxDiv v (digit radix v) + n)) with (S (maxDiv v (digit radix v)) + n); auto. rewrite Zpower_nat_is_exp. repeat rewrite (fun x : Z => Zmult_comm x (Zpower_nat radix n)). red in |- *; intros H'. absurd (Zdivides v (Zpower_nat radix (S (maxDiv v (digit radix v))))). case (maxDivUniqueDigit v); auto. apply ZdividesDiv with (p := Zpower_nat radix n); auto with zarith. apply sym_not_eq, Z.lt_neq, Zpower_nat_less; easy. apply digitAdd; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz