proposition: Theorem pPredMoreThanRadix : (radix < pPred (vNum b))%Z.
proof: Proof. apply Z.le_lt_trans with (nNormMin radix precision). pattern radix at 1 in |- *; rewrite <- (Zpower_nat_1 radix); unfold nNormMin in |- *; auto with zarith. apply Zpower_nat_monotone_le; lia. apply nNormMimLtvNum; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz