proposition: Theorem PosNormMin : Zpos (vNum b) = (radix * nNormMin)%Z.
proof: Proof. pattern radix at 1 in |- *; rewrite <- (Zpower_nat_1 radix); unfold nNormMin in |- *. rewrite pGivesBound; rewrite <- Zpower_nat_is_exp. generalize precisionNotZero; case precision; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz