proposition: Theorem FnormalLtFirstNormalPos : forall p : float, Fnormal p -> (0 <= p)%R -> (firstNormalPos <= p)%R.
proof: Proof. intros p H' H'0. case (Rle_or_lt firstNormalPos p); intros Lt0; auto with real. case (FnormalLtPos p firstNormalPos); auto. apply firstNormalPosNormal. intros H'1; contradict H'1; unfold firstNormalPos in |- *; simpl in |- *. apply Zle_not_lt; apply H'. intros H'1; elim H'1; intros H'2 H'3; contradict H'3. unfold firstNormalPos in |- *; simpl in |- *. apply Zle_not_lt. rewrite <- (Z.abs_eq (Fnum p)); auto with zarith. apply pNormal_absolu_min; auto. apply LeR0Fnum with (radix := radix); auto with arith. Qed.
imports: Reals ZArith List PeanoNat Psatz