proposition: Theorem pSubnormal_absolu_min : forall p : float, Fsubnormal p -> (Z.abs (Fnum p) < nNormMin)%Z.
proof: Proof. intros p H'; apply Zlt_mult_simpl_l with (c := radix); auto with zarith. replace (radix * Z.abs (Fnum p))%Z with (Z.abs (radix * Fnum p)). replace (radix * nNormMin)%Z with (Zpos (vNum b)); try apply H'. rewrite pGivesBound. replace precision with (1 + pred precision). rewrite Zpower_nat_is_exp; auto with zarith; rewrite Zpower_nat_1; auto. generalize precisionNotZero; case precision; simpl in |- *; auto. intros H; contradict H; auto. rewrite Zabs_Zmult; rewrite (Z.abs_eq radix); auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz