proposition: Theorem maxDivUniqueInverseDigit : forall (v : Z) (p : nat), v <> 0 -> Zdivides v (Zpower_nat radix p) -> ~ Zdivides v (Zpower_nat radix (S p)) -> p = maxDiv v (digit radix v).
proof: Proof. intros v p H' H'0 H'1. apply maxDivSimplInv; auto. 2: apply maxDivUniqueInverse; auto. apply Zpower_nat_anti_monotone_lt with (n := radix); auto. apply Z.le_lt_trans with (m := Z.abs v); auto. rewrite <- (fun x => Z.abs_eq (Zpower_nat radix x)); try apply ZDividesLe; auto. apply Zpower_NR0; lia. apply digitMore; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz