proposition: Theorem nNrMMimLevNum : (nNormMin <= Zpos (vNum b))%Z.
proof: Proof. rewrite pGivesBound. unfold nNormMin in |- *; simpl in |- *; auto with zarith arith. apply Zpower_nat_monotone_le; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz