proposition: Theorem FboundNext : forall p : float, Fbounded b p -> exists q : float, Fbounded b q /\ q = Float (Z.succ (Fnum p)) (Fexp p) :>R.
proof: Proof. intros p H'. case (Zle_lt_or_eq (Z.succ (Fnum p)) (Zpos (vNum b))). case (Zle_or_lt 0 (Fnum p)); intros H1. rewrite <- (Z.abs_eq (Fnum p)); auto with zarith. generalize (proj1 H'); auto with zarith. apply Z.le_trans with 0%Z; auto with zarith. intros H'0; exists (Float (Z.succ (Fnum p)) (Fexp p)); split; auto. repeat split; simpl in |- *; try apply H'; auto with zarith. case (Zle_or_lt 0 (Fnum p)); intros H1; try lia. apply Z.lt_trans with (Z.abs (Fnum p)); try apply H'; auto with zarith. repeat rewrite Zabs_eq_opp; auto with zarith. intros H'0; exists (Float (Zpower_nat radix (pred precision)) (Z.succ (Fexp p))); split; auto. repeat split; simpl in |- *; auto with zarith arith. rewrite pGivesBound. rewrite Z.abs_eq; auto with zarith. apply Zpower_nat_monotone_lt; auto with zarith. apply Zpower_NR0; auto with zarith. generalize (proj2 H'); auto with zarith. rewrite H'0; rewrite pGivesBound. pattern precision at 2 in |- *; replace precision with (1 + pred precision). rewrite Zpower_nat_is_exp. rewrite Zpower_nat_1. unfold FtoRradix, FtoR in |- *; simpl in |- *. rewrite powerRZ_Zs. rewrite mult_IZR; ring. apply IZR_neq; auto with zarith. generalize precisionNotZero; case precision; simpl in |- *; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz