proposition: Theorem FsubnormalLtFirstNormalPos : forall p : float, Fsubnormal p -> (0 <= p)%R -> (p < firstNormalPos)%R.
proof: Proof. intros p H' H'0; unfold FtoRradix, FtoR, firstNormalPos in |- *; simpl in |- *. replace (Fexp p) with (- dExp b)%Z. 2: apply sym_equal; case H'; intros H1 H2; case H2; auto. apply Rmult_lt_compat_r; auto with real arith. apply powerRZ_lt, IZR_lt; easy. apply IZR_lt. rewrite <- (Z.abs_eq (Fnum p)). 2: apply LeR0Fnum with (radix := radix); auto with zarith. apply pSubnormal_absolu_min; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz