proposition: Theorem RND_Min_Pos_Rle : forall r : R, (0 <= r)%R -> (RND_Min_Pos r <= r)%R.
proof: Proof. intros r H. unfold RND_Min_Pos in |- *; case (Rle_dec (firstNormalPos radix b p) r); intros H2. unfold FtoRradix, FtoR in |- *; simpl in |- *. apply Rle_trans with (r * powerRZ radix (- IRNDD (ln r / ln radix + (- Z.pred p)%Z)) * powerRZ radix (IRNDD (ln r / ln radix + (- Z.pred p)%Z)))%R; auto with real. apply Rmult_le_compat_r. apply powerRZ_le, IZR_lt; lia. apply IRNDD_correct1. rewrite Rmult_assoc; rewrite <- powerRZ_add; try apply IZR_neq; auto with real zarith. ring_simplify (- IRNDD (ln r / ln radix + (- Z.pred p)%Z) + IRNDD (ln r / ln radix + (- Z.pred p)%Z))%Z; simpl in |- *; auto with real. unfold FtoRradix, FtoR in |- *; simpl in |- *. apply Rle_trans with (r * powerRZ radix (dExp b) * powerRZ radix (- dExp b))%R; auto with real. apply Rmult_le_compat_r. apply powerRZ_le, IZR_lt; lia. apply IRNDD_correct1. rewrite Rmult_assoc; rewrite <- powerRZ_add; try apply IZR_neq; auto with real zarith. ring_simplify (dExp b + - dExp b)%Z; simpl in |- *; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz