proposition: Theorem ZltNormMinVnum : (nNormMin radix precision < Zpos (vNum b))%Z.
proof: Proof. unfold nNormMin in |- *; rewrite pGivesBound; auto with zarith. apply Zpower_nat_monotone_lt; lia. Qed.
imports: Reals ZArith List PeanoNat Psatz