proposition: Theorem FSuccSubnormNearNormMin : forall a : float, Fsubnormal radix b a -> Fnum a = Z.pred (nNormMin radix precision) -> Fnormal radix b (FSucc a).
proof: Proof. intros a H' H'0. cut (Fbounded b a); [ intros Fb0 | apply FsubnormalFbounded with (1 := H') ]. unfold FSucc in |- *. generalize (Z_eq_bool_correct (Fnum a) (pPred (vNum b))); case (Z_eq_bool (Fnum a) (pPred (vNum b))); auto. intros H'1; absurd (nNormMin radix precision < Zpos (vNum b))%Z. 2: apply ZltNormMinVnum. apply Zle_not_lt. apply Zle_n_Zpred; unfold pPred in H'1; rewrite <- H'1; rewrite H'0; auto with zarith. intros H'3; generalize (Z_eq_bool_correct (Fnum a) (- nNormMin radix precision)); case (Z_eq_bool (Fnum a) (- nNormMin radix precision)). intros H'1; absurd (- nNormMin radix precision < Z.pred (nNormMin radix precision))%Z. rewrite <- H'1; rewrite <- H'0; auto with zarith. unfold nNormMin in |- *; apply Z.lt_le_trans with (m := (- (0))%Z); auto with zarith. intros H'4; repeat split; simpl in |- *; auto with zarith arith; try apply Fb0. rewrite H'0. rewrite <- Zsucc_pred. rewrite Z.abs_eq; auto with zarith. apply ZltNormMinVnum. apply Zlt_le_weak, nNormPos; easy. rewrite H'0. rewrite <- Zsucc_pred. pattern radix at 1 in |- *; rewrite <- (Zpower_nat_1 radix); unfold nNormMin in |- *; rewrite <- Zpower_nat_is_exp. rewrite pGivesBound. rewrite Z.abs_eq. generalize precisionNotZero; case precision; simpl in |- *; auto with zarith. apply Zpower_NR0; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz