proposition: Theorem RND_Min_Pos_bounded_aux : forall (r : R) (e : Z), (0 <= r)%R -> (- dExp b <= e)%Z -> (r < powerRZ radix (e + p))%R -> Fbounded b (Float (IRNDD (r * powerRZ radix (- e))) e).
proof: Proof. intros r e H1 H2 H3. split; auto. simpl in |- *; rewrite pGivesBound; apply lt_IZR. rewrite Zpower_nat_Z_powerRZ; rewrite <- Rabs_Zabs. rewrite Rabs_right; [ idtac | apply Rle_ge; apply IRNDD_pos; apply Rmult_le_pos; auto with real zarith ]. apply Rle_lt_trans with (1 := IRNDD_correct1 (r * powerRZ radix (- e))). apply Rmult_lt_reg_l with (powerRZ radix e); auto with zarith real. apply powerRZ_lt, IZR_lt; lia. rewrite Rmult_comm; rewrite Rmult_assoc. rewrite <- powerRZ_add; try apply IZR_neq; auto with zarith real. rewrite <- powerRZ_add; try apply IZR_neq; auto with zarith real. apply Rle_lt_trans with (2 := H3); ring_simplify (- e + e)%Z; simpl in |- *; right; ring. apply powerRZ_le, IZR_lt; lia. Qed.
imports: Reals ZArith List PeanoNat Psatz