proposition: Theorem FBoundedSuc : forall f : float, Fbounded b f -> Fbounded b (FSucc f).
proof: Proof. intros f H'; unfold FSucc in |- *. generalize (Z_eq_bool_correct (Fnum f) (pPred (vNum b))); case (Z_eq_bool (Fnum f) (pPred (vNum b))); intros H'1. repeat split; simpl in |- *. rewrite Z.abs_eq. apply ZltNormMinVnum. apply Zlt_le_weak, nNormPos; easy. apply Z.le_trans with (Fexp f); auto with zarith; apply H'. generalize (Z_eq_bool_correct (Fnum f) (- nNormMin radix precision)); case (Z_eq_bool (Fnum f) (- nNormMin radix precision)); intros H'2. generalize (Z_eq_bool_correct (Fexp f) (- dExp b)); case (Z_eq_bool (Fexp f) (- dExp b)); intros H'3. repeat split; simpl in |- *; auto with zarith arith. apply Zlt_Zabs_Zpred; auto with zarith arith. apply H'. repeat split; simpl in |- *; auto with zarith arith. rewrite Zabs_Zopp. rewrite Z.abs_eq; unfold pPred in |- *; lia. generalize (proj2 H'); lia. repeat split; simpl in |- *; try apply H'. apply Zlt_Zabs_Zpred; try apply H'; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz