fact: Fixpoint maxDiv (v : Z) (p : nat) {struct p} : nat := match p with | O => 0 | S p' => match ZdividesP v (Zpower_nat radix p) with | left _ => p | right _ => maxDiv v p' end end.
imports: Reals ZArith List PeanoNat Psatz