proposition: Theorem FSuccSubnormNotNearNormMin : forall a : float, Fsubnormal radix b a -> Fnum a <> Z.pred (nNormMin radix precision) -> Fsubnormal radix b (FSucc a).
proof: Proof. intros a H' H'0. cut (Fbounded b a); [ intros B0 | apply FsubnormalFbounded with (1 := H'); auto ]. 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'2; absurd (Fdigit radix a < precision). 2: apply FsubnormalDigit with (b := b); auto. unfold Fdigit in |- *; rewrite H'2. unfold pPred in |- *; rewrite (digitPredVNumiSPrecision radix) with (b := b) (precision := precision); auto with arith. intros H'3; generalize (Z_eq_bool_correct (Fnum a) (- nNormMin radix precision)); case (Z_eq_bool (Fnum a) (- nNormMin radix precision)). intros H'2; absurd (Fdigit radix a < precision). unfold Fdigit in |- *; rewrite H'2. replace (digit radix (- nNormMin radix precision)) with (digit radix (nNormMin radix precision)). rewrite digitnNormMin; auto with arith. case (nNormMin radix precision); simpl in |- *; auto. apply FsubnormalDigit with (b := b); auto. intros H'4; repeat split; simpl in |- *; auto with zarith arith; try apply H'. apply Z.le_lt_trans with (m := Z.succ (Z.abs (Fnum a))). apply Zabs_Zs. apply Z.lt_le_trans with (m := Z.succ (nNormMin radix precision)). apply Zsucc_lt_compat; apply pSubnormal_absolu_min with (3 := pGivesBound); auto with zarith arith. case H'; intros H1 (H2, H3). apply Zlt_le_succ,ZltNormMinVnum. rewrite Zabs_Zmult. rewrite (Z.abs_eq radix); auto with zarith. apply Z.lt_le_trans with (m := (radix * nNormMin radix precision)%Z). apply Zmult_gt_0_lt_compat_l; try apply Z.lt_gt; auto with zarith. apply Zlt_Zabs_Zpred; auto with zarith arith. apply pSubnormal_absolu_min with (3 := pGivesBound); auto. pattern radix at 1 in |- *; rewrite <- (Zpower_nat_1 radix); unfold nNormMin in |- *; rewrite <- Zpower_nat_is_exp. rewrite pGivesBound. generalize precisionNotZero; case precision; simpl in |- *; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz