proposition: Theorem FnormalNnormMin : forall x : Z, (- dExp b <= x)%Z -> Fnormal (Float nNormMin x).
proof: Proof. intros x H; (cut (0 < nNormMin)%Z; [ intros Z1 | apply nNormPos ]). repeat split; simpl in |- *; auto with zarith. rewrite Z.abs_eq; auto with zarith. rewrite PosNormMin. pattern nNormMin at 1 in |- *; replace nNormMin with (1 * nNormMin)%Z; auto with zarith. apply Zmult_gt_0_lt_compat_r; auto with zarith. rewrite PosNormMin; lia. Qed.
imports: Reals ZArith List PeanoNat Psatz