proposition: Theorem FSuccNormNegNotNormMin : forall a : float, (a <= 0)%R -> Fnormal radix b a -> a <> Float (- nNormMin radix precision) (- dExp b) -> Fnormal radix b (FSucc a).
proof: Proof. intros a H' H'0 H'1; cut (Fbounded b a); [ intros Fb0 | apply FnormalBounded with (1 := H'0) ]. cut (Fnum a <= 0)%Z; [ intros Z0 | apply R0LeFnum with (radix := radix) ]; auto with zarith. case (Zle_lt_or_eq _ _ Z0); intros Z1. 2: absurd (is_Fzero a). 2: apply FnormalNotZero with (1 := H'0); 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 (0 < Fnum a)%Z; auto with zarith arith. rewrite H'2; unfold pPred in |- *; apply Zlt_succ_pred; simpl in |- *; apply (vNumbMoreThanOne radix) with (precision := precision); auto with zarith arith. intros H'3; generalize (Z_eq_bool_correct (Fnum a) (- nNormMin radix precision)); case (Z_eq_bool (Fnum a) (- nNormMin radix precision)); auto. intros H'2; generalize (Z_eq_bool_correct (Fexp a) (- dExp b)); case (Z_eq_bool (Fexp a) (- dExp b)). intros H'4; contradict H'1; auto. apply floatEq; auto. intros H'4; repeat split; simpl in |- *; auto with zarith. rewrite Zabs_Zopp. unfold pPred in |- *; rewrite Z.abs_eq; auto with zarith. apply Zle_Zpred; auto with zarith. case (Zle_next (- dExp b) (Fexp a)); try apply Fb0; auto with zarith. rewrite <- Zopp_mult_distr_r; rewrite Zabs_Zopp. rewrite Zabs_Zmult. repeat rewrite Z.abs_eq; auto with zarith. pattern (Zpos (vNum b)) at 1 in |- *; rewrite (PosNormMin radix) with (precision := precision); auto with zarith. apply Zle_Zmult_comp_l; auto with zarith. unfold pPred in |- *; apply Zle_Zpred; auto with zarith. apply ZltNormMinVnum. apply Zle_Zpred; auto with zarith. intros H'2; repeat split; simpl in |- *; auto with zarith arith. apply Z.lt_trans with (Z.abs (Fnum a)); try apply Fb0. repeat rewrite Zabs_eq_opp; auto with zarith. apply Fb0. rewrite Zabs_Zmult. rewrite (Z.abs_eq radix); [ idtac | apply Z.le_trans with 1%Z; auto with zarith ]. repeat rewrite Zabs_eq_opp; auto with zarith. pattern (Zpos (vNum b)) at 1 in |- *; rewrite (PosNormMin radix) with (precision := precision); auto with zarith. apply Zle_Zmult_comp_l; auto with zarith. replace (- Z.succ (Fnum a))%Z with (Z.pred (- Fnum a)). case (Zle_lt_or_eq (nNormMin radix precision) (- Fnum a)); auto with zarith. rewrite <- Zabs_eq_opp; auto with zarith. apply pNormal_absolu_min with (b := b); auto. apply Zpred_Zopp_Zs; auto. apply is_Fzero_rep2 with radix; try easy. unfold FtoR; rewrite Z1; simpl; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz