proposition: Theorem FSuccNormNegNormMin : Fsubnormal radix b (FSucc (Float (- nNormMin radix precision) (- dExp b))).
proof: Proof. unfold FSucc in |- *; simpl in |- *. generalize (Z_eq_bool_correct (- nNormMin radix precision) (pPred (vNum b))); case (Z_eq_bool (- nNormMin radix precision) (pPred (vNum b))); intros H'; auto. absurd (0 < pPred (vNum b))%Z; auto. rewrite <- H'; auto with zarith. change 0%Z with (- (0))%Z. apply Zle_not_lt; apply Zle_Zopp, Zlt_le_weak. apply nNormPos; auto with zarith. unfold pPred in |- *; apply Zlt_succ_pred; simpl in |- *; auto with zarith. apply (vNumbMoreThanOne radix) with (precision := precision); auto with zarith. generalize (Z_eq_bool_correct (- nNormMin radix precision) (- nNormMin radix precision)); case (Z_eq_bool (- nNormMin radix precision) (- nNormMin radix precision)); intros H'0. 2: contradict H'0; auto. generalize (Z_eq_bool_correct (- dExp b) (- dExp b)); case (Z_eq_bool (- dExp b) (- dExp b)); intros H'1. 2: contradict H'1; auto. repeat split; simpl in |- *; auto with zarith. apply Z.le_lt_trans with (m := nNormMin radix precision); auto with zarith. rewrite <- Zopp_Zpred_Zs; rewrite Zabs_Zopp; rewrite Z.abs_eq; auto with zarith. apply Zle_Zpred; simpl in |- *; auto with zarith. apply nNormPos; auto with zarith. apply ZltNormMinVnum. rewrite Zabs_Zmult; rewrite (Z.abs_eq radix); auto with zarith. rewrite (PosNormMin radix) with (precision := precision); auto with zarith. apply Zmult_gt_0_lt_compat_l; auto with zarith. rewrite <- Zopp_Zpred_Zs; rewrite Zabs_Zopp. rewrite Z.abs_eq; auto with zarith. apply Zle_Zpred; simpl in |- *; auto with zarith. apply nNormPos; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz